Theorem 1oex 8447

Description: Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) Remove dependency on ax-10 2175, ax-11 2191, ax-12 2212, ax-un 7718. (Revised by Zhi Wang, 19-Sep-2024.)

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8444	. 2 ⊢ 1o = {∅}
2		snex 5396	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2858	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2142  Vcvv 3454  ∅c0 4285  {csn 4582  1_oc1o 8430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-un 3909  df-nul 4286  df-sn 4583  df-pr 4585  df-suc 6352  df-1o 8437

This theorem is referenced by:  1oelpr  8448  1on  8450  nlim2  8459  oev  8483  oe0  8491  oev2  8492  oneo  8550  nnneo  8625  enpr2d  9029  endisj  9036  map2xp  9119  snnen2o  9189  sdom1  9194  rex2dom  9197  1sdom2dom  9198  ssttrcl  9670  ttrclselem2  9681  djuexb  9867  djurcl  9869  djurf1o  9871  djuss  9878  djuun  9884  1stinr  9887  2ndinr  9888  pm54.43  9959  dju1dif  10129  djucomen  10134  djuassen  10135  infdju1  10146  pwdju1  10147  nnadju  10154  infmap2  10173  cfsuc  10214  isfin4p1  10272  dcomex  10404  pwcfsdom  10541  cfpwsdom  10542  canthp1lem2  10611  pwxpndom2  10623  indpi  10865  pinq  10885  archnq  10938  sadcf  16487  sadcp1  16489  fnpr2ob  17588  xpsfrnel  17592  xpsle  17609  setcepi  18121  setc2obas  18127  setc2ohom  18128  efgi1  19761  frgpuptinv  19811  dmdprdpr  20091  dprdpr  20092  coe1fval3  22267  00ply1bas  22298  ply1plusgfvi  22300  coe1z  22323  coe1tm  22333  ply1vscl  22441  rhmply1  22443  rhmply1vr1  22444  xpstopnlem1  23866  xpstopnlem2  23868  xpsdsval  24438  nofv  27718  noxp1o  27724  noextendlt  27730  bdayfo  27738  nosep1o  27742  nosepdmlem  27744  nolt02o  27756  nogt01o  27757  nosupbnd1lem5  27773  nosupbnd2lem1  27776  noinfno  27779  noinfbday  27781  noinfbnd1  27790  noinfbnd2lem1  27791  noinfbnd2  27792  noetasuplem1  27794  noetasuplem2  27795  noetasuplem4  27797  fply1  33751  selvply1rhmlema  33812  selvply1rhmlemb  33813  selvply1rhmlem1  33814  selvply1rhmlem2  33815  selvply1rhmlem4  33817  selvply1rhm0  33820  gonanegoal  35699  fmlaomn0  35737  gonan0  35739  gonarlem  35741  gonar  35742  fmlasucdisj  35746  satffunlem  35748  satffunlem2lem1  35751  ex-sategoelel12  35774  rankeq1o  36518  bj-pr2val  37500  bj-2upln1upl  37506  rhmpsr1  43163  pw2f1ocnv  43611  omnord1ex  43878  oege2  43881  oenord1ex  43889  oenord1  43890  oenassex  43892  cantnfresb  43898  omcl3g  43908  clsk3nimkb  44613  clsk1indlem4  44617  clsk1indlem1  44618  f1omo  49511  f1omoOLD  49512  f1omoALT  49513  nelsubc3  49689  indthinc  50080  indthincALT  50081  prsthinc  50082  setc1obas  50110  setc1ohomfval  50111  setc1oid  50113  isinito2lem  50116  isinito3  50118  prstchom  50180  prstchom2ALT  50182  setc1onsubc  50220  cnelsubc  50222