Theorem dfss3f

Description: Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 20-Mar-2004)

	Ref	Expression
Hypotheses	dfss2f.1	$$⊢\underset{\_}{Ⅎ}xA$$
	dfss2f.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	dfss3f	$$⊢A\subseteq B\leftrightarrow \forall x\in Ax\in B$$

Proof

Step	Hyp	Ref	Expression
1		dfss2f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dfss2f.2	$$⊢\underset{\_}{Ⅎ}xB$$
3	1 2	dfss2f	$$⊢A\subseteq B\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$
4		df-ral	$$⊢\forall x\in Ax\in B\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$
5	3 4	bitr4i	$$⊢A\subseteq B\leftrightarrow \forall x\in Ax\in B$$