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

Metamath Proof Explorer

Theorem ideqg

Description: For sets, the identity relation is the same as equality. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion ideqg 
|- ( B e. V -> ( A _I B <-> A = B ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( B e. V -> B e. V )
2 reli 
 |-  Rel _I
3 2 brrelex1i 
 |-  ( A _I B -> A e. _V )
4 1 3 anim12ci 
 |-  ( ( B e. V /\ A _I B ) -> ( A e. _V /\ B e. V ) )
5 eleq1 
 |-  ( A = B -> ( A e. V <-> B e. V ) )
6 5 biimparc 
 |-  ( ( B e. V /\ A = B ) -> A e. V )
7 6 elexd 
 |-  ( ( B e. V /\ A = B ) -> A e. _V )
8 simpl 
 |-  ( ( B e. V /\ A = B ) -> B e. V )
9 7 8 jca 
 |-  ( ( B e. V /\ A = B ) -> ( A e. _V /\ B e. V ) )
10 eqeq1 
 |-  ( x = A -> ( x = y <-> A = y ) )
11 eqeq2 
 |-  ( y = B -> ( A = y <-> A = B ) )
12 df-id 
 |-  _I = { <. x , y >. | x = y }
13 10 11 12 brabg 
 |-  ( ( A e. _V /\ B e. V ) -> ( A _I B <-> A = B ) )
14 4 9 13 pm5.21nd 
 |-  ( B e. V -> ( A _I B <-> A = B ) )