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

Metamath Proof Explorer

Theorem eqvincg

Description: A variable introduction law for class equality, closed form. (Contributed by Thierry Arnoux, 2-Mar-2017)

Ref Expression
Assertion eqvincg 
|- ( A e. V -> ( A = B <-> E. x ( x = A /\ x = B ) ) )

Proof

Step Hyp Ref Expression
1 elisset 
 |-  ( A e. V -> E. x x = A )
2 ax-1 
 |-  ( x = A -> ( A = B -> x = A ) )
3 eqtr 
 |-  ( ( x = A /\ A = B ) -> x = B )
4 3 ex 
 |-  ( x = A -> ( A = B -> x = B ) )
5 2 4 jca 
 |-  ( x = A -> ( ( A = B -> x = A ) /\ ( A = B -> x = B ) ) )
6 5 eximi 
 |-  ( E. x x = A -> E. x ( ( A = B -> x = A ) /\ ( A = B -> x = B ) ) )
7 pm3.43 
 |-  ( ( ( A = B -> x = A ) /\ ( A = B -> x = B ) ) -> ( A = B -> ( x = A /\ x = B ) ) )
8 7 eximi 
 |-  ( E. x ( ( A = B -> x = A ) /\ ( A = B -> x = B ) ) -> E. x ( A = B -> ( x = A /\ x = B ) ) )
9 1 6 8 3syl 
 |-  ( A e. V -> E. x ( A = B -> ( x = A /\ x = B ) ) )
10 19.37v 
 |-  ( E. x ( A = B -> ( x = A /\ x = B ) ) <-> ( A = B -> E. x ( x = A /\ x = B ) ) )
11 9 10 sylib 
 |-  ( A e. V -> ( A = B -> E. x ( x = A /\ x = B ) ) )
12 eqtr2 
 |-  ( ( x = A /\ x = B ) -> A = B )
13 12 exlimiv 
 |-  ( E. x ( x = A /\ x = B ) -> A = B )
14 11 13 impbid1 
 |-  ( A e. V -> ( A = B <-> E. x ( x = A /\ x = B ) ) )