Theorem ctex 8526

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 8517	. 2 ⊢ Rel ≼
2	1	brrelex1i 5610	1 ⊢ (𝐴 ≼ ω → 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3496   class class class wbr 5068  ωcom 7582   ≼ cdom 8509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-rel 5564  df-dom 8513

This theorem is referenced by:  cnvct  8588  ssct  8600  xpct  9444  iunfictbso  9542  unctb  9629  dmct  9948  fimact  9959  fnct  9961  mptct  9962  iunctb  9998  cctop  21616  1stcrestlem  22062  2ndcdisj2  22067  dis2ndc  22070  uniiccdif  24181  mptctf  30455  elsigagen2  31409  measvunilem  31473  measvunilem0  31474  measvuni  31475  sxbrsigalem1  31545  omssubadd  31560  carsggect  31578  pmeasadd  31585  mpct  41471  axccdom  41494