Theorem kardcard2a

Description: If two sets have equal nonzero card cardinalities, then they have equal kard cardinalities. This theorem does not depend on the Axiom of Choice. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	kardcard2a	⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ∅ ) → ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		carden2a	⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ∅ ) → 𝐴 ≈ 𝐵 )
2		fvfundmfvn0	⊢ ( ( card ‘ 𝐴 ) ≠ ∅ → ( 𝐴 ∈ dom card ∧ Fun ( card ↾ { 𝐴 } ) ) )
3	2	simpld	⊢ ( ( card ‘ 𝐴 ) ≠ ∅ → 𝐴 ∈ dom card )
4		kardeng	⊢ ( 𝐴 ∈ dom card → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
5	3 4	syl	⊢ ( ( card ‘ 𝐴 ) ≠ ∅ → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
6	5	adantl	⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ∅ ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
7	1 6	mpbird	⊢ ( ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐴 ) ≠ ∅ ) → ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) )