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	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		reldom	⊢ Rel ≼
2	1	brrelex1i	⊢ ( 𝐴 ≼ ω → 𝐴 ∈ V )