Metamath Proof Explorer

Theorem idssen

Description: Equality implies equinumerosity. (Contributed by NM, 30-Apr-1998) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion idssen 
|- _I C_ ~~

Proof

Step Hyp Ref Expression
1 reli 
 |-  Rel _I
2 vex 
 |-  y e. _V
3 2 ideq 
 |-  ( x _I y <-> x = y )
4 eqeng 
 |-  ( x e. _V -> ( x = y -> x ~~ y ) )
5 4 elv 
 |-  ( x = y -> x ~~ y )
6 3 5 sylbi 
 |-  ( x _I y -> x ~~ y )
7 df-br 
 |-  ( x _I y <-> <. x , y >. e. _I )
8 df-br 
 |-  ( x ~~ y <-> <. x , y >. e. ~~ )
9 6 7 8 3imtr3i 
 |-  ( <. x , y >. e. _I -> <. x , y >. e. ~~ )
10 1 9 relssi 
 |-  _I C_ ~~