Theorem 1oex 6528

Description: Ordinal 1 is a set. (Contributed by BJ, 4-Jul-2022.)

Assertion

Ref	Expression
1oex	⊢ 1o ∈ V

Proof of Theorem 1oex

Step	Hyp	Ref	Expression
1		1on 6527	. 2 ⊢ 1o ∈ On
2	1	elexi 2786	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2177  Vcvv 2773  Oncon0 4423  1_oc1o 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4173  ax-nul 4181  ax-pow 4229  ax-pr 4264  ax-un 4493

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ral 2490  df-rex 2491  df-v 2775  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-nul 3465  df-pw 3623  df-sn 3644  df-pr 3645  df-uni 3860  df-tr 4154  df-iord 4426  df-on 4428  df-suc 4431  df-1o 6520

This theorem is referenced by:  1lt2o  6546  map1  6923  rex2dom  6929  1domsn  6934  pw1fin  7028  exmidpw2en  7030  djuexb  7167  djurclr  7173  djurcl  7175  djurf1or  7180  djurf1o  7182  djuss  7193  infnninf  7247  infnninfOLD  7248  ismkvnex  7278  pr2cv1  7324  dju1p1e2  7331  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  djucomen  7354  djuassen  7355  pw1on  7367  pw1nel3  7372  sucpw1ne3  7373  sucpw1nel3  7374  fmelpw1o  7388  indpi  7485  prarloclemlt  7636  fxnn0nninf  10616  inftonninf  10619  nninfctlemfo  12446  nninfct  12447  enctlem  12888  fnpr2ob  13257  xpsfrnel  13261  djurclALT  15908  bj-charfun  15912  pw1map  16104  pw1mapen  16105  pwle2  16107  pw1nct  16112  nnnninfex  16131  nninfnfiinf  16132