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

Proof

Step	Hyp	Ref	Expression
1		carden2a	|- ( ( ( card ` A ) = ( card ` B ) /\ ( card ` A ) =/= (/) ) -> A ~~ B )
2		fvfundmfvn0	|- ( ( card ` A ) =/= (/) -> ( A e. dom card /\ Fun ( card |` { A } ) ) )
3	2	simpld	|- ( ( card ` A ) =/= (/) -> A e. dom card )
4		kardeng	|- ( A e. dom card -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )
5	3 4	syl	|- ( ( card ` A ) =/= (/) -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )
6	5	adantl	|- ( ( ( card ` A ) = ( card ` B ) /\ ( card ` A ) =/= (/) ) -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) )
7	1 6	mpbird	|- ( ( ( card ` A ) = ( card ` B ) /\ ( card ` A ) =/= (/) ) -> ( kard ` A ) = ( kard ` B ) )