Theorem 1oex 6655

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 6654	. 2 ⊢ 1o ∈ On
2	1	elexi 2826	1 ⊢ 1o ∈ V

Syntax hints:   ∈ wcel 2203  Vcvv 2813  Oncon0 4484  1_oc1o 6640

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-sep 4228  ax-nul 4236  ax-pow 4287  ax-pr 4322  ax-un 4554

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-rex 2526  df-v 2815  df-dif 3213  df-un 3215  df-in 3217  df-ss 3224  df-nul 3509  df-pw 3671  df-sn 3695  df-pr 3696  df-uni 3915  df-tr 4209  df-iord 4487  df-on 4489  df-suc 4492  df-1o 6647

This theorem is referenced by:  2oex  6664  1lt2o  6675  map1  7054  modom  7061  rex2dom  7063  1domsn  7068  pw1fin  7170  exmidpw2en  7172  djuexb  7335  djurclr  7341  djurcl  7343  djurf1or  7348  djurf1o  7350  djuss  7361  infnninf  7415  infnninfOLD  7416  ismkvnex  7446  pr2cv1  7492  dju1p1e2  7500  exmidfodomrlemr  7505  exmidfodomrlemrALT  7506  djucomen  7523  djuassen  7524  pw1on  7536  pw1nel3  7541  sucpw1ne3  7542  sucpw1nel3  7543  fmelpw1o  7557  indpi  7657  prarloclemlt  7808  fxnn0nninf  10801  inftonninf  10804  nninfctlemfo  12736  nninfct  12737  enctlem  13183  fnpr2ob  13553  xpsfrnel  13557  djurclALT  16574  bj-charfun  16577  pw1map  16769  pw1mapen  16770  pwle2  16772  pw1nct  16777  pw1dceq  16778  exmidcon  16780  nnnninfex  16800  nninfnfiinf  16801