Theorem ctex

Description: A countable set is a set. (Contributed by Thierry Arnoux, 29-Dec-2016) (Proof shortened by Jim Kingdon, 13-Mar-2023)

	Ref	Expression
Assertion	ctex	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		reldom	$$⊢\mathrm{Rel}\preccurlyeq$$
2	1	brrelex1i	$$⊢A\preccurlyeq \mathrm{\omega }\to A\in \mathrm{V}$$