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 ) )