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	|- ( x = A -> ( ( kard ` x ) = ( kard ` B ) <-> ( kard ` A ) = ( kard ` B ) ) )
2		breq1	|- ( x = A -> ( x ~~ B <-> A ~~ B ) )
3		vex	|- x e. _V
4		kardval	|- ( kard ` x ) = Scott { y | y ~~ x }
5		kardval	|- ( kard ` B ) = Scott { y | y ~~ B }
6	3 4 5	karden	|- ( ( kard ` x ) = ( kard ` B ) <-> x ~~ B )
7	1 2 6	vtoclbg	|- ( A e. V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )