Theorem dfssf

Description: Equivalence for subclass relation, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 3-Jul-1994) (Revised by Andrew Salmon, 27-Aug-2011) Avoid ax-13 . (Revised by Gino Giotto, 19-May-2023)

	Ref	Expression
Hypotheses	dfssf.1	$$⊢\underset{\_}{Ⅎ}xA$$
	dfssf.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	dfssf	$$⊢A\subseteq B\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfssf.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		dfssf.2	$$⊢\underset{\_}{Ⅎ}xB$$
3		df-ss	$$⊢A\subseteq B\leftrightarrow \forall z\left(z\in A\to z\in B\right)$$
4	1	nfcri	$$⊢Ⅎxz\in A$$
5	2	nfcri	$$⊢Ⅎxz\in B$$
6	4 5	nfim	$$⊢Ⅎx\left(z\in A\to z\in B\right)$$
7		nfv	$$⊢Ⅎz\left(x\in A\to x\in B\right)$$
8		eleq1w	$$⊢z=x\to \left(z\in A\leftrightarrow x\in A\right)$$
9		eleq1w	$$⊢z=x\to \left(z\in B\leftrightarrow x\in B\right)$$
10	8 9	imbi12d	$$⊢z=x\to \left(\left(z\in A\to z\in B\right)\leftrightarrow \left(x\in A\to x\in B\right)\right)$$
11	6 7 10	cbvalv1	$$⊢\forall z\left(z\in A\to z\in B\right)\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$
12	3 11	bitri	$$⊢A\subseteq B\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$