Metamath Proof Explorer

Theorem kardenir

Description: If two sets are equinumerous, then their kard cardinal numbers are equal. (Contributed by BTernaryTau, 4-Jul-2026)

Ref Expression
Assertion kardenir 
|- ( A ~~ B -> ( kard ` A ) = ( kard ` B ) )

Proof

Step Hyp Ref Expression
1 relen 
 |-  Rel ~~
2 1 brrelex1i 
 |-  ( A ~~ B -> A e. _V )
3 kardeng 
 |-  ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )
4 2 3 syl 
 |-  ( A ~~ B -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )
5 4 ibir 
 |-  ( A ~~ B -> ( kard ` A ) = ( kard ` B ) )