Theorem kardsn

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

	Ref	Expression
Assertion	kardsn	Could not format assertion : No typesetting found for |- ( A e. V -> ( kard ` { A } ) = ( kard ` 1o ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		ensn1g	$$⊢A\in V\to \left\{A\right\}\approx 1_{𝑜}$$
2		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
3		kardeng	Could not format ( { A } e. _V -> ( ( kard ` { A } ) = ( kard ` 1o ) <-> { A } ~~ 1o ) ) : No typesetting found for |- ( { A } e. _V -> ( ( kard ` { A } ) = ( kard ` 1o ) <-> { A } ~~ 1o ) ) with typecode |-
4	2 3	ax-mp	Could not format ( ( kard ` { A } ) = ( kard ` 1o ) <-> { A } ~~ 1o ) : No typesetting found for |- ( ( kard ` { A } ) = ( kard ` 1o ) <-> { A } ~~ 1o ) with typecode |-
5	1 4	sylibr	Could not format ( A e. V -> ( kard ` { A } ) = ( kard ` 1o ) ) : No typesetting found for |- ( A e. V -> ( kard ` { A } ) = ( kard ` 1o ) ) with typecode |-