df-sub

Definition.

Arguments:

a (st), b (st), x (sv),

Distinct variable conditions:

(x, a), (x, b),

Assertions:

((asubseteqb)leftrightarrowforallx((xina)to(xinb)))