Metamath Proof Explorer

Theorem ennum

Description: Equinumerous sets are equi-numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion ennum 
|- ( A ~~ B -> ( A e. dom card <-> B e. dom card ) )

Proof

Step Hyp Ref Expression
1 enen2 
 |-  ( A ~~ B -> ( x ~~ A <-> x ~~ B ) )
2 1 rexbidv 
 |-  ( A ~~ B -> ( E. x e. On x ~~ A <-> E. x e. On x ~~ B ) )
3 isnum2 
 |-  ( A e. dom card <-> E. x e. On x ~~ A )
4 isnum2 
 |-  ( B e. dom card <-> E. x e. On x ~~ B )
5 2 3 4 3bitr4g 
 |-  ( A ~~ B -> ( A e. dom card <-> B e. dom card ) )