Theorem ctex 8379

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

Assertion

Ref	Expression
ctex	⊢ (𝐴 ≼ ω → 𝐴 ∈ V)

Proof of Theorem ctex

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

Syntax hints:   → wi 4   ∈ wcel 2083  Vcvv 3440   class class class wbr 4968  ωcom 7443   ≼ cdom 8362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-sn 4479  df-pr 4481  df-op 4485  df-br 4969  df-opab 5031  df-xp 5456  df-rel 5457  df-dom 8366

This theorem is referenced by:  cnvct  8441  ssct  8452  xpct  9295  iunfictbso  9393  unctb  9480  dmct  9799  fimact  9810  fnct  9812  mptct  9813  iunctb  9849  cctop  21302  1stcrestlem  21748  2ndcdisj2  21753  dis2ndc  21756  uniiccdif  23866  mptctf  30137  elsigagen2  31020  measvunilem  31084  measvunilem0  31085  measvuni  31086  sxbrsigalem1  31156  omssubadd  31171  carsggect  31189  pmeasadd  31196  mpct  41025  axccdom  41048