Theorem 1oex 8444

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8441	. 2 ⊢ 1o = {∅}
2		snex 5391	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2824	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ∅c0 4296  {csn 4589  1_oc1o 8427

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-nul 4297  df-sn 4590  df-pr 4592  df-suc 6338  df-1o 8434

This theorem is referenced by:  1on  8446  nlim2  8454  oev  8478  oe0  8486  oev2  8487  oneo  8545  nnneo  8619  enpr2d  9020  endisj  9028  map2xp  9111  snnen2o  9184  sdom1  9189  sdom1OLD  9190  rex2dom  9193  1sdom2dom  9194  1sdomOLD  9196  ssttrcl  9668  ttrclselem2  9679  djuexb  9862  djurcl  9864  djurf1o  9866  djuss  9873  djuun  9879  1stinr  9882  2ndinr  9883  pm54.43  9954  dju1dif  10126  djucomen  10131  djuassen  10132  infdju1  10143  pwdju1  10144  nnadju  10151  infmap2  10170  cfsuc  10210  isfin4p1  10268  dcomex  10400  pwcfsdom  10536  cfpwsdom  10537  canthp1lem2  10606  pwxpndom2  10618  indpi  10860  pinq  10880  archnq  10933  sadcf  16423  sadcp1  16425  fnpr2ob  17521  xpsfrnel  17525  xpsle  17542  setcepi  18050  setc2obas  18056  setc2ohom  18057  efgi1  19651  frgpuptinv  19701  dmdprdpr  19981  dprdpr  19982  coe1fval3  22093  00ply1bas  22124  ply1plusgfvi  22126  coe1z  22149  coe1tm  22159  ply1vscl  22271  rhmply1  22273  rhmply1vr1  22274  xpstopnlem1  23696  xpstopnlem2  23698  xpsdsval  24269  nofv  27569  noxp1o  27575  noextendlt  27581  bdayfo  27589  nosep1o  27593  nosepdmlem  27595  nolt02o  27607  nogt01o  27608  nosupbnd1lem5  27624  nosupbnd2lem1  27627  noinfno  27630  noinfbday  27632  noinfbnd1  27641  noinfbnd2lem1  27642  noinfbnd2  27643  noetasuplem1  27645  noetasuplem2  27646  noetasuplem4  27648  fply1  33527  gonanegoal  35339  fmlaomn0  35377  gonan0  35379  gonarlem  35381  gonar  35382  fmlasucdisj  35386  satffunlem  35388  satffunlem2lem1  35391  ex-sategoelel12  35414  rankeq1o  36159  bj-pr2val  37006  bj-2upln1upl  37012  rhmpsr1  42541  pw2f1ocnv  43026  omnord1ex  43293  oege2  43296  oenord1ex  43304  oenord1  43305  oaomoencom  43306  oenassex  43307  cantnfresb  43313  omcl3g  43323  clsk3nimkb  44029  clsk1indlem4  44033  clsk1indlem1  44034  f1omo  48881  f1omoOLD  48882  f1omoALT  48883  nelsubc3  49060  indthinc  49451  indthincALT  49452  prsthinc  49453  setc1obas  49481  setc1ohomfval  49482  setc1oid  49484  isinito2lem  49487  isinito3  49489  prstchom  49551  prstchom2ALT  49553  setc1onsubc  49591  cnelsubc  49593