Theorem kardcard

Description: Two sets have equal kard cardinalities iff they have equal card cardinalities. This theorem depends on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardcard	Could not format assertion : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		axac3	$$⊢\mathrm{CHOICE}$$
2		ackardcard	Could not format ( CHOICE -> ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) ) : No typesetting found for |- ( CHOICE -> ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) ) with typecode |-
3	1 2	ax-mp	Could not format ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) : No typesetting found for |- ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) with typecode |-