Theorem ctex 8912

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

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   class class class wbr 5100  ωcom 7818   ≼ cdom 8893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-rel 5639  df-dom 8897

This theorem is referenced by:  cnvct  8983  xpct  9938  iunfictbso  10036  unctb  10126  dmct  10446  fimact  10457  fnct  10459  mptct  10460  iunctb  10497  cctop  22962  1stcrestlem  23408  2ndcdisj2  23413  dis2ndc  23416  uniiccdif  25547  mptctf  32805  elsigagen2  34325  measvunilem  34389  measvunilem0  34390  measvuni  34391  sxbrsigalem1  34462  omssubadd  34477  carsggect  34495  pmeasadd  34502  mpct  45553  axccdom  45574  rn1st  45625