Theorem eqvincf

Description: A variable introduction law for class equality, using bound-variable hypotheses instead of distinct variable conditions. (Contributed by NM, 14-Sep-2003)

	Ref	Expression
Hypotheses	eqvincf.1	|- F/_ x A
	eqvincf.2	|- F/_ x B
	eqvincf.3	|- A e. _V
Assertion	eqvincf	|- ( A = B <-> E. x ( x = A /\ x = B ) )

Proof

Step	Hyp	Ref	Expression
1		eqvincf.1	|- F/_ x A
2		eqvincf.2	|- F/_ x B
3		eqvincf.3	|- A e. _V
4	3	eqvinc	|- ( A = B <-> E. y ( y = A /\ y = B ) )
5	1	nfeq2	|- F/ x y = A
6	2	nfeq2	|- F/ x y = B
7	5 6	nfan	|- F/ x ( y = A /\ y = B )
8		nfv	|- F/ y ( x = A /\ x = B )
9		eqeq1	|- ( y = x -> ( y = A <-> x = A ) )
10		eqeq1	|- ( y = x -> ( y = B <-> x = B ) )
11	9 10	anbi12d	|- ( y = x -> ( ( y = A /\ y = B ) <-> ( x = A /\ x = B ) ) )
12	7 8 11	cbvexv1	|- ( E. y ( y = A /\ y = B ) <-> E. x ( x = A /\ x = B ) )
13	4 12	bitri	|- ( A = B <-> E. x ( x = A /\ x = B ) )