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	|- F/_ x A
	dfss2f.2	|- F/_ x B
Assertion	dfss3f	|- ( A C_ B <-> A. x e. A x e. B )

Proof

Step	Hyp	Ref	Expression
1		dfss2f.1	|- F/_ x A
2		dfss2f.2	|- F/_ x B
3	1 2	dfss2f	|- ( A C_ B <-> A. x ( x e. A -> x e. B ) )
4		df-ral	|- ( A. x e. A x e. B <-> A. x ( x e. A -> x e. B ) )
5	3 4	bitr4i	|- ( A C_ B <-> A. x e. A x e. B )