This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )