Theorem 1oex 6568

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

Syntax hints:   ∈ wcel 2200  Vcvv 2799  Oncon0 4453  1_oc1o 6553

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4201  ax-nul 4209  ax-pow 4257  ax-pr 4292  ax-un 4523

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-rex 2514  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-nul 3492  df-pw 3651  df-sn 3672  df-pr 3673  df-uni 3888  df-tr 4182  df-iord 4456  df-on 4458  df-suc 4461  df-1o 6560

This theorem is referenced by:  1lt2o  6586  map1  6963  rex2dom  6969  1domsn  6974  pw1fin  7068  exmidpw2en  7070  djuexb  7207  djurclr  7213  djurcl  7215  djurf1or  7220  djurf1o  7222  djuss  7233  infnninf  7287  infnninfOLD  7288  ismkvnex  7318  pr2cv1  7364  dju1p1e2  7371  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  djucomen  7394  djuassen  7395  pw1on  7407  pw1nel3  7412  sucpw1ne3  7413  sucpw1nel3  7414  fmelpw1o  7428  indpi  7525  prarloclemlt  7676  fxnn0nninf  10656  inftonninf  10659  nninfctlemfo  12556  nninfct  12557  enctlem  12998  fnpr2ob  13368  xpsfrnel  13372  djurclALT  16124  bj-charfun  16128  pw1map  16320  pw1mapen  16321  pwle2  16323  pw1nct  16328  nnnninfex  16347  nninfnfiinf  16348