Metamath Proof Explorer


Theorem elrncard

Description: Let us define a cardinal number to be an element A e. On such that A is not equipotent with any x e. A . (Contributed by RP, 1-Oct-2023)

Ref Expression
Assertion elrncard
|- ( A e. ran card <-> ( A e. On /\ A. x e. A -. x ~~ A ) )

Proof

Step Hyp Ref Expression
1 iscard4
 |-  ( ( card ` A ) = A <-> A e. ran card )
2 iscard5
 |-  ( ( card ` A ) = A <-> ( A e. On /\ A. x e. A -. x ~~ A ) )
3 1 2 bitr3i
 |-  ( A e. ran card <-> ( A e. On /\ A. x e. A -. x ~~ A ) )