Theorem kardeng

Description: Two sets are equinumerous iff their kard cardinal numbers are equal. Unlike carden , this theorem does not depend on the Axiom of Choice, but it does depend on the Axiom of Regularity and the Axiom of Infinity. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardeng	|- ( A e. V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	|- ( z = A -> ( ( kard ` z ) = ( kard ` B ) <-> ( kard ` A ) = ( kard ` B ) ) )
2		breq1	|- ( z = A -> ( z ~~ B <-> A ~~ B ) )
3		vex	|- z e. _V
4		kardval2	|- ( kard ` z ) = { x | ( x ~~ z /\ A. y ( y ~~ z -> ( rank ` x ) C_ ( rank ` y ) ) ) }
5		kardval2	|- ( kard ` B ) = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) }
6	3 4 5	karden	|- ( ( kard ` z ) = ( kard ` B ) <-> z ~~ B )
7	1 2 6	vtoclbg	|- ( A e. V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )