Metamath Proof Explorer

Theorem eqeng

Description: Equality implies equinumerosity. (Contributed by NM, 26-Oct-2003)

Ref Expression
Assertion eqeng 
|- ( A e. V -> ( A = B -> A ~~ B ) )

Proof

Step Hyp Ref Expression
1 enrefg 
 |-  ( A e. V -> A ~~ A )
2 breq2 
 |-  ( A = B -> ( A ~~ A <-> A ~~ B ) )
3 1 2 syl5ibcom 
 |-  ( A e. V -> ( A = B -> A ~~ B ) )