Theorem ctex 8969

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146  Vcvv 3458   class class class wbr 5114  ωcom 7871   ≼ cdom 8950

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-ral 3083  df-rex 3093  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-rel 5673  df-dom 8954

This theorem is used by:  cnvct  9041  xpct  10019  iunfictbso  10117  unctb  10206  dmct  10526  fimact  10537  fnct  10539  mptct  10540  iunctb  10577  cctop  23200  1stcrestlem  23646  2ndcdisj2  23651  dis2ndc  23654  uniiccdif  25774  mptctf  33098  elsigagen2  34570  measvunilem  34634  measvunilem0  34635  measvuni  34636  sxbrsigalem1  34707  omssubadd  34722  carsggect  34740  pmeasadd  34747  mpct  45959  axccdom  45979  rn1st  46029