Theorem ackardcard

Description: The Axiom of Choice implies that two sets have equal kard cardinalities iff they have equal card cardinalities. (Contributed by BTernaryTau, 3-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		acnum	|- ( CHOICE -> ( A e. V -> A e. dom card ) )
2		acnum	|- ( CHOICE -> ( B e. W -> B e. dom card ) )
3	1 2	anim12d	|- ( CHOICE -> ( ( A e. V /\ B e. W ) -> ( A e. dom card /\ B e. dom card ) ) )
4		kardcard2	|- ( ( A e. dom card /\ B e. dom card ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) )
5	3 4	syl6	|- ( CHOICE -> ( ( A e. V /\ B e. W ) -> ( ( kard ` A ) = ( kard ` B ) <-> ( card ` A ) = ( card ` B ) ) ) )