Theorem kardenir

Description: If two sets are equinumerous, then their kard cardinal numbers are equal. (Contributed by BTernaryTau, 4-Jul-2026)

	Ref	Expression
Assertion	kardenir	Could not format assertion : No typesetting found for |- ( A ~~ B -> ( kard ` A ) = ( kard ` B ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		relen	$$⊢\mathrm{Rel}\approx$$
2	1	brrelex1i	$$⊢A\approx B\to A\in \mathrm{V}$$
3		kardeng	Could not format ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) : No typesetting found for |- ( A e. _V -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) with typecode |-
4	2 3	syl	Could not format ( A ~~ B -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) : No typesetting found for |- ( A ~~ B -> ( ( kard ` A ) = ( kard ` B ) <-> A ~~ B ) ) with typecode |-
5	4	ibir	Could not format ( A ~~ B -> ( kard ` A ) = ( kard ` B ) ) : No typesetting found for |- ( A ~~ B -> ( kard ` A ) = ( kard ` B ) ) with typecode |-