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	⊢ ( 𝐴 ≈ 𝐵 → ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		relen	⊢ Rel ≈
2	1	brrelex1i	⊢ ( 𝐴 ≈ 𝐵 → 𝐴 ∈ V )
3		kardeng	⊢ ( 𝐴 ∈ V → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
4	2 3	syl	⊢ ( 𝐴 ≈ 𝐵 → ( ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) ↔ 𝐴 ≈ 𝐵 ) )
5	4	ibir	⊢ ( 𝐴 ≈ 𝐵 → ( kard ‘ 𝐴 ) = ( kard ‘ 𝐵 ) )