Theorem kardex

Description: The collection of all sets equinumerous to a set A and having the least possible rank is a set. This is the part of the justification of the definition of kard of Enderton p. 222. (Contributed by NM, 14-Dec-2003) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026)

	Ref	Expression
Assertion	kardex	|- Scott { x | x ~~ A } e. _V

Proof

Step	Hyp	Ref	Expression
1		scottex	|- Scott { x | x ~~ A } e. _V