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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		axac3	⊢ CHOICE
2		ackardcard	⊢ ( CHOICE → ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) ) )
3	1 2	ax-mp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )