Theorem 1oex 8415

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8412	. 2 ⊢ 1o = {∅}
2		snex 5381	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2832	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ∅c0 4273  {csn 4567  1_oc1o 8398

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-sn 4568  df-pr 4570  df-suc 6329  df-1o 8405

This theorem is referenced by:  1on  8417  nlim2  8425  oev  8449  oe0  8457  oev2  8458  oneo  8516  nnneo  8591  enpr2d  8995  endisj  9002  map2xp  9085  snnen2o  9155  sdom1  9160  rex2dom  9163  1sdom2dom  9164  ssttrcl  9636  ttrclselem2  9647  djuexb  9833  djurcl  9835  djurf1o  9837  djuss  9844  djuun  9850  1stinr  9853  2ndinr  9854  pm54.43  9925  dju1dif  10095  djucomen  10100  djuassen  10101  infdju1  10112  pwdju1  10113  nnadju  10120  infmap2  10139  cfsuc  10179  isfin4p1  10237  dcomex  10369  pwcfsdom  10506  cfpwsdom  10507  canthp1lem2  10576  pwxpndom2  10588  indpi  10830  pinq  10850  archnq  10903  sadcf  16422  sadcp1  16424  fnpr2ob  17522  xpsfrnel  17526  xpsle  17543  setcepi  18055  setc2obas  18061  setc2ohom  18062  efgi1  19696  frgpuptinv  19746  dmdprdpr  20026  dprdpr  20027  coe1fval3  22172  00ply1bas  22203  ply1plusgfvi  22205  coe1z  22228  coe1tm  22238  ply1vscl  22349  rhmply1  22351  rhmply1vr1  22352  xpstopnlem1  23774  xpstopnlem2  23776  xpsdsval  24346  nofv  27621  noxp1o  27627  noextendlt  27633  bdayfo  27641  nosep1o  27645  nosepdmlem  27647  nolt02o  27659  nogt01o  27660  nosupbnd1lem5  27676  nosupbnd2lem1  27679  noinfno  27682  noinfbday  27684  noinfbnd1  27693  noinfbnd2lem1  27694  noinfbnd2  27695  noetasuplem1  27697  noetasuplem2  27698  noetasuplem4  27700  fply1  33618  gonanegoal  35534  fmlaomn0  35572  gonan0  35574  gonarlem  35576  gonar  35577  fmlasucdisj  35581  satffunlem  35583  satffunlem2lem1  35586  ex-sategoelel12  35609  rankeq1o  36353  bj-pr2val  37325  bj-2upln1upl  37331  rhmpsr1  42996  pw2f1ocnv  43465  omnord1ex  43732  oege2  43735  oenord1ex  43743  oenord1  43744  oaomoencom  43745  oenassex  43746  cantnfresb  43752  omcl3g  43762  clsk3nimkb  44467  clsk1indlem4  44471  clsk1indlem1  44472  f1omo  49368  f1omoOLD  49369  f1omoALT  49370  nelsubc3  49546  indthinc  49937  indthincALT  49938  prsthinc  49939  setc1obas  49967  setc1ohomfval  49968  setc1oid  49970  isinito2lem  49973  isinito3  49975  prstchom  50037  prstchom2ALT  50039  setc1onsubc  50077  cnelsubc  50079