Metamath Proof Explorer
Description: A countable set is a set. (Contributed by Thierry Arnoux, 29Dec2016)
(Proof shortened by Jim Kingdon, 13Mar2023)


Ref 
Expression 

Assertion 
ctex 
$${\u22a2}{A}\preccurlyeq \mathrm{\omega}\to {A}\in \mathrm{V}$$ 
Proof
Step 
Hyp 
Ref 
Expression 
1 

reldom 
$${\u22a2}\mathrm{Rel}\preccurlyeq $$ 
2 
1

brrelex1i 
$${\u22a2}{A}\preccurlyeq \mathrm{\omega}\to {A}\in \mathrm{V}$$ 