Theorem ctex 8938

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

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   class class class wbr 5110  ωcom 7845   ≼ cdom 8919

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-rel 5648  df-dom 8923

This theorem is referenced by:  cnvct  9008  ssctOLD  9026  xpct  9976  iunfictbso  10074  unctb  10164  dmct  10484  fimact  10495  fnct  10497  mptct  10498  iunctb  10534  cctop  22900  1stcrestlem  23346  2ndcdisj2  23351  dis2ndc  23354  uniiccdif  25486  mptctf  32648  elsigagen2  34145  measvunilem  34209  measvunilem0  34210  measvuni  34211  sxbrsigalem1  34283  omssubadd  34298  carsggect  34316  pmeasadd  34323  mpct  45202  axccdom  45223  rn1st  45274