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 GG, 19-May-2023)

	Ref	Expression
Hypotheses	dfssf.1	|- F/_ x A
	dfssf.2	|- F/_ x B
Assertion	dfssf	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )

Proof

Step	Hyp	Ref	Expression
1		dfssf.1	|- F/_ x A
2		dfssf.2	|- F/_ x B
3		df-ss	|- ( A C_ B <-> A. z ( z e. A -> z e. B ) )
4	1	nfcri	|- F/ x z e. A
5	2	nfcri	|- F/ x z e. B
6	4 5	nfim	|- F/ x ( z e. A -> z e. B )
7		nfv	|- F/ z ( x e. A -> x e. B )
8		eleq1w	|- ( z = x -> ( z e. A <-> x e. A ) )
9		eleq1w	|- ( z = x -> ( z e. B <-> x e. B ) )
10	8 9	imbi12d	|- ( z = x -> ( ( z e. A -> z e. B ) <-> ( x e. A -> x e. B ) ) )
11	6 7 10	cbvalv1	|- ( A. z ( z e. A -> z e. B ) <-> A. x ( x e. A -> x e. B ) )
12	3 11	bitri	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )