Metamath Proof Explorer

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	\|- ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		axac3	\|- CHOICE
2		ackardcard	\|- ( CHOICE -> ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) )
3	1 2	ax-mp	\|- ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) )

Step

Hyp

Ref

Expression

axac3

 |-  CHOICE

ackardcard

 |-  ( CHOICE -> ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) )

1 2

ax-mp

 |-  ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) )