Theorem 1oex 8498

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8495	. 2 ⊢ 1o = {∅}
2		snex 5429	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2822	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2099  Vcvv 3462  ∅c0 4322  {csn 4623  1_oc1o 8481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697  ax-sep 5296  ax-nul 5303  ax-pr 5425

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-v 3464  df-dif 3949  df-un 3951  df-nul 4323  df-sn 4624  df-pr 4626  df-suc 6374  df-1o 8488

This theorem is referenced by:  1on  8500  2oexOLD  8509  nlim2  8512  oev  8536  oe0  8544  oev2  8545  oneo  8603  nnneo  8677  enpr2d  9079  endisj  9088  map2xp  9177  snnen2o  9264  sdom1  9269  sdom1OLD  9270  rex2dom  9273  1sdom2dom  9274  1sdomOLD  9276  ssttrcl  9751  ttrclselem2  9762  djuexb  9945  djurcl  9947  djurf1o  9949  djuss  9956  djuun  9962  1stinr  9965  2ndinr  9966  pm54.43  10037  dju1dif  10208  djucomen  10213  djuassen  10214  infdju1  10225  pwdju1  10226  nnadju  10233  infmap2  10252  cfsuc  10291  isfin4p1  10349  dcomex  10481  pwcfsdom  10617  cfpwsdom  10618  canthp1lem2  10687  pwxpndom2  10699  indpi  10941  pinq  10961  archnq  11014  sadcf  16448  sadcp1  16450  fnpr2ob  17568  xpsfrnel  17572  xpsle  17589  setcepi  18105  setc2obas  18111  setc2ohom  18112  efgi1  19715  frgpuptinv  19765  dmdprdpr  20045  dprdpr  20046  coe1fval3  22194  00ply1bas  22225  ply1plusgfvi  22227  coe1z  22250  coe1tm  22260  ply1vscl  22372  rhmply1  22374  rhmply1vr1  22375  xpstopnlem1  23801  xpstopnlem2  23803  xpsdsval  24375  nofv  27684  noxp1o  27690  noextendlt  27696  bdayfo  27704  nosep1o  27708  nosepdmlem  27710  nolt02o  27722  nogt01o  27723  nosupbnd1lem5  27739  nosupbnd2lem1  27742  noinfno  27745  noinfbday  27747  noinfbnd1  27756  noinfbnd2lem1  27757  noinfbnd2  27758  noetasuplem1  27760  noetasuplem2  27761  noetasuplem4  27763  fply1  33437  gonanegoal  35193  fmlaomn0  35231  gonan0  35233  gonarlem  35235  gonar  35236  fmlasucdisj  35240  satffunlem  35242  satffunlem2lem1  35245  ex-sategoelel12  35268  rankeq1o  36008  bj-pr2val  36738  bj-2upln1upl  36744  rhmpsr1  42243  pw2f1ocnv  42732  omnord1ex  43007  oege2  43010  oenord1ex  43018  oenord1  43019  oaomoencom  43020  oenassex  43021  cantnfresb  43027  omcl3g  43037  clsk3nimkb  43744  clsk1indlem4  43748  clsk1indlem1  43749  f1omo  48264  f1omoALT  48265  indthinc  48409  indthincALT  48410  prsthinc  48411  prstchom  48434  prstchom2ALT  48436