MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ctex Structured version   Visualization version   GIF version

Theorem ctex 8511
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
StepHypRef Expression
1 reldom 8502 . 2 Rel ≼
21brrelex1i 5576 1 (𝐴 ≼ ω → 𝐴 ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2112  Vcvv 3444   class class class wbr 5033  ωcom 7564  cdom 8494
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-br 5034  df-opab 5096  df-xp 5529  df-rel 5530  df-dom 8498
This theorem is referenced by:  cnvct  8573  ssct  8585  xpct  9431  iunfictbso  9529  unctb  9620  dmct  9939  fimact  9950  fnct  9952  mptct  9953  iunctb  9989  cctop  21614  1stcrestlem  22060  2ndcdisj2  22065  dis2ndc  22068  uniiccdif  24185  mptctf  30482  elsigagen2  31515  measvunilem  31579  measvunilem0  31580  measvuni  31581  sxbrsigalem1  31651  omssubadd  31666  carsggect  31684  pmeasadd  31691  mpct  41817  axccdom  41840
  Copyright terms: Public domain W3C validator