MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1oex Structured version   Visualization version   GIF version

Theorem 1oex 8423
Description: Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) Remove dependency on ax-10 2138, ax-11 2155, ax-12 2172, ax-un 7673. (Revised by Zhi Wang, 19-Sep-2024.)
Assertion
Ref Expression
1oex 1o ∈ V

Proof of Theorem 1oex
StepHypRef Expression
1 df1o2 8420 . 2 1o = {∅}
2 snex 5389 . 2 {∅} ∈ V
31, 2eqeltri 2834 1 1o ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3446  c0 4283  {csn 4587  1oc1o 8406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-sep 5257  ax-nul 5264  ax-pr 5385
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-dif 3914  df-un 3916  df-nul 4284  df-sn 4588  df-pr 4590  df-suc 6324  df-1o 8413
This theorem is referenced by:  1on  8425  2oexOLD  8434  nlim2  8437  oev  8461  oe0  8469  oev2  8470  oneo  8529  nnneo  8602  enpr2d  8994  endisj  9003  map2xp  9092  snnen2o  9182  sdom1  9187  sdom1OLD  9188  rex2dom  9191  1sdom2dom  9192  1sdomOLD  9194  ssttrcl  9652  ttrclselem2  9663  djuexb  9846  djurcl  9848  djurf1o  9850  djuss  9857  djuun  9863  1stinr  9866  2ndinr  9867  pm54.43  9938  dju1dif  10109  djucomen  10114  djuassen  10115  infdju1  10126  pwdju1  10127  nnadju  10134  infmap2  10155  cfsuc  10194  isfin4p1  10252  dcomex  10384  pwcfsdom  10520  cfpwsdom  10521  canthp1lem2  10590  pwxpndom2  10602  indpi  10844  pinq  10864  archnq  10917  sadcf  16334  sadcp1  16336  fnpr2ob  17441  xpsfrnel  17445  xpsle  17462  setcepi  17975  setc2obas  17981  setc2ohom  17982  efgi1  19504  frgpuptinv  19554  dmdprdpr  19829  dprdpr  19830  coe1fval3  21582  00ply1bas  21614  ply1plusgfvi  21616  coe1z  21637  coe1tm  21647  xpstopnlem1  23163  xpstopnlem2  23165  xpsdsval  23737  nofv  27008  noxp1o  27014  noextendlt  27020  bdayfo  27028  nosep1o  27032  nosepdmlem  27034  nolt02o  27046  nogt01o  27047  nosupbnd1lem5  27063  nosupbnd2lem1  27066  noinfno  27069  noinfbday  27071  noinfbnd1  27080  noinfbnd2lem1  27081  noinfbnd2  27082  noetasuplem1  27084  noetasuplem2  27085  noetasuplem4  27087  fply1  32268  gonanegoal  33949  fmlaomn0  33987  gonan0  33989  gonarlem  33991  gonar  33992  fmlasucdisj  33996  satffunlem  33998  satffunlem2lem1  34001  ex-sategoelel12  34024  rankeq1o  34759  bj-pr2val  35492  bj-2upln1upl  35498  pw2f1ocnv  41364  omnord1ex  41641  oege2  41644  oenord1ex  41652  oenord1  41653  oaomoencom  41654  oenassex  41655  cantnfresb  41661  omcl3g  41670  clsk3nimkb  42319  clsk1indlem4  42323  clsk1indlem1  42324  f1omo  46934  f1omoALT  46935  indthinc  47079  indthincALT  47080  prsthinc  47081  prstchom  47104  prstchom2ALT  47106
  Copyright terms: Public domain W3C validator