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

Proof

Step	Hyp	Ref	Expression
1		kardeng	|- ( A e. dom card -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )
2	1	adantr	|- ( ( A e. dom card /\ B e. dom card ) -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )
3		carden2	|- ( ( A e. dom card /\ B e. dom card ) -> ( ( card ` A ) = ( card ` B ) <-> A ~~ B ) )
4	2 3	bitr4d	|- ( ( A e. dom card /\ B e. dom card ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) )