Theorem 1oex 7968

Description: Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.)

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		1on 7967	. 2 ⊢ 1o ∈ On
2	1	elexi 3459	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2083  Vcvv 3440  Oncon0 6073  1_oc1o 7953

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pr 5228  ax-un 7326

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3or 1081  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-pss 3882  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-tp 4483  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-tr 5071  df-eprel 5360  df-po 5369  df-so 5370  df-fr 5409  df-we 5411  df-ord 6076  df-on 6077  df-suc 6079  df-1o 7960

This theorem is referenced by:  2oex  7970  oev  7997  oe0  8005  oev2  8006  oneo  8064  nnneo  8135  endisj  8458  map2xp  8541  sdom1  8571  1sdom  8574  djuexb  9191  djurcl  9193  djurf1o  9195  djuss  9202  djuun  9208  1stinr  9211  2ndinr  9212  pm54.43  9282  dju1dif  9451  djucomen  9456  djuassen  9457  infdju1  9468  pwdju1  9469  infmap2  9493  cfsuc  9532  isfin4p1  9590  dcomex  9722  pwcfsdom  9858  cfpwsdom  9859  canthp1lem2  9928  pwxpndom2  9940  indpi  10182  pinq  10202  archnq  10255  sadcf  15639  sadcp1  15641  fnpr2ob  16664  xpsfrnel  16668  xpsle  16685  setcepi  17181  efgi1  18578  frgpuptinv  18628  dmdprdpr  18892  dprdpr  18893  coe1fval3  20063  00ply1bas  20095  ply1plusgfvi  20097  coe1z  20118  coe1tm  20128  xpstopnlem1  22105  xpstopnlem2  22107  xpsdsval  22678  fply1  30575  gonanegoal  32209  fmlaomn0  32247  gonan0  32249  gonarlem  32251  gonar  32252  fmlasucdisj  32256  satffunlem  32258  satffunlem2lem1  32261  ex-sategoelel12  32284  nofv  32775  noxp1o  32781  noextendlt  32787  bdayfo  32793  nosep1o  32797  nosepdmlem  32798  nolt02o  32810  nosupbnd1lem5  32823  nosupbnd2lem1  32826  noetalem1  32828  noetalem3  32830  noetalem4  32831  rankeq1o  33243  bj-pr2val  33956  bj-2upln1upl  33962  pw2f1ocnv  39140  clsk3nimkb  39896  clsk1indlem4  39900  clsk1indlem1  39901