Theorem kardcard2

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

	Ref	Expression
Assertion	kardcard2	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		kardeng	⊢ ( 𝐴 ∈ dom card → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
2	1	adantr	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
3		carden2	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
4	2 3	bitr4d	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝐵 ) ) )