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 ( x = A -> ( ( kard ` x ) = ( kard ` B ) <-> ( kard ` A ) = ( kard ` B ) ) ) : No typesetting found for |- ( x = A -> ( ( kard ` x ) = ( kard ` B ) <-> ( kard ` A ) = ( kard ` B ) ) ) with typecode |-
2		breq1	$$⊢x=A\to \left(x\approx B\leftrightarrow A\approx B\right)$$
3		vex	$$⊢x\in \mathrm{V}$$
4		kardval	Could not format ( kard ` x ) = Scott { y | y ~~ x } : No typesetting found for |- ( kard ` x ) = Scott { y | y ~~ x } with typecode |-
5		kardval	Could not format ( kard ` B ) = Scott { y | y ~~ B } : No typesetting found for |- ( kard ` B ) = Scott { y | y ~~ B } with typecode |-
6	3 4 5	karden	Could not format ( ( kard ` x ) = ( kard ` B ) <-> x ~~ B ) : No typesetting found for |- ( ( kard ` x ) = ( kard ` B ) <-> x ~~ 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 |-