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	Could not format assertion : No typesetting found for |- ( A e. V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	Could not format ( z = A -> ( ( kard ` z ) = ( kard ` B ) <-> ( kard ` A ) = ( kard ` B ) ) ) : No typesetting found for |- ( z = A -> ( ( kard ` z ) = ( kard ` B ) <-> ( kard ` A ) = ( kard ` B ) ) ) with typecode |-
2		breq1	$$⊢z=A\to \left(z\approx B\leftrightarrow A\approx B\right)$$
3		vex	$$⊢z\in \mathrm{V}$$
4		kardval2	Could not format ( kard ` z ) = { x | ( x ~~ z /\ A. y ( y ~~ z -> ( rank ` x ) C_ ( rank ` y ) ) ) } : No typesetting found for |- ( kard ` z ) = { x | ( x ~~ z /\ A. y ( y ~~ z -> ( rank ` x ) C_ ( rank ` y ) ) ) } with typecode |-
5		kardval2	Could not format ( kard ` B ) = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) } : No typesetting found for |- ( kard ` B ) = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) } with typecode |-
6	3 4 5	karden	Could not format ( ( kard ` z ) = ( kard ` B ) <-> z ~~ B ) : No typesetting found for |- ( ( kard ` z ) = ( kard ` B ) <-> z ~~ B ) with typecode |-
7	1 2 6	vtoclbg	Could not format ( A e. V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) : No typesetting found for |- ( A e. V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) with typecode |-