Theorem kardsn

Description: A singleton has cardinality one. (Contributed by BTernaryTau, 4-Jul-2026)

	Ref	Expression
Assertion	kardsn	⊢ ( 𝐴 ∈ 𝑉 → ( kard ‘ { 𝐴 } ) = ( kard ‘ 1o ) )

Proof

Step	Hyp	Ref	Expression
1		ensn1g	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≈ 1o )
2		snex	⊢ { 𝐴 } ∈ V
3		kardeng	⊢ ( { 𝐴 } ∈ V → ( ( kard ‘ { 𝐴 } ) = ( kard ‘ 1o ) ↔ { 𝐴 } ≈ 1o ) )
4	2 3	ax-mp	⊢ ( ( kard ‘ { 𝐴 } ) = ( kard ‘ 1o ) ↔ { 𝐴 } ≈ 1o )
5	1 4	sylibr	⊢ ( 𝐴 ∈ 𝑉 → ( kard ‘ { 𝐴 } ) = ( kard ‘ 1o ) )