Theorem 1oex 8532

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

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		df1o2 8529	. 2 ⊢ 1o = {∅}
2		snex 5451	. 2 ⊢ {∅} ∈ V
3	1, 2	eqeltri 2840	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ∅c0 4352  {csn 4648  1_oc1o 8515

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-sn 4649  df-pr 4651  df-suc 6401  df-1o 8522

This theorem is referenced by:  1on  8534  2oexOLD  8543  nlim2  8546  oev  8570  oe0  8578  oev2  8579  oneo  8637  nnneo  8711  enpr2d  9115  endisj  9124  map2xp  9213  snnen2o  9300  sdom1  9305  sdom1OLD  9306  rex2dom  9309  1sdom2dom  9310  1sdomOLD  9312  ssttrcl  9784  ttrclselem2  9795  djuexb  9978  djurcl  9980  djurf1o  9982  djuss  9989  djuun  9995  1stinr  9998  2ndinr  9999  pm54.43  10070  dju1dif  10242  djucomen  10247  djuassen  10248  infdju1  10259  pwdju1  10260  nnadju  10267  infmap2  10286  cfsuc  10326  isfin4p1  10384  dcomex  10516  pwcfsdom  10652  cfpwsdom  10653  canthp1lem2  10722  pwxpndom2  10734  indpi  10976  pinq  10996  archnq  11049  sadcf  16499  sadcp1  16501  fnpr2ob  17618  xpsfrnel  17622  xpsle  17639  setcepi  18155  setc2obas  18161  setc2ohom  18162  efgi1  19763  frgpuptinv  19813  dmdprdpr  20093  dprdpr  20094  coe1fval3  22231  00ply1bas  22262  ply1plusgfvi  22264  coe1z  22287  coe1tm  22297  ply1vscl  22409  rhmply1  22411  rhmply1vr1  22412  xpstopnlem1  23838  xpstopnlem2  23840  xpsdsval  24412  nofv  27720  noxp1o  27726  noextendlt  27732  bdayfo  27740  nosep1o  27744  nosepdmlem  27746  nolt02o  27758  nogt01o  27759  nosupbnd1lem5  27775  nosupbnd2lem1  27778  noinfno  27781  noinfbday  27783  noinfbnd1  27792  noinfbnd2lem1  27793  noinfbnd2  27794  noetasuplem1  27796  noetasuplem2  27797  noetasuplem4  27799  fply1  33549  gonanegoal  35320  fmlaomn0  35358  gonan0  35360  gonarlem  35362  gonar  35363  fmlasucdisj  35367  satffunlem  35369  satffunlem2lem1  35372  ex-sategoelel12  35395  rankeq1o  36135  bj-pr2val  36984  bj-2upln1upl  36990  rhmpsr1  42508  pw2f1ocnv  42994  omnord1ex  43266  oege2  43269  oenord1ex  43277  oenord1  43278  oaomoencom  43279  oenassex  43280  cantnfresb  43286  omcl3g  43296  clsk3nimkb  44002  clsk1indlem4  44006  clsk1indlem1  44007  f1omo  48574  f1omoALT  48575  indthinc  48719  indthincALT  48720  prsthinc  48721  prstchom  48744  prstchom2ALT  48746