Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 1oex | Structured version Visualization version GIF version |
Description: Ordinal 1 is a set. (Contributed by BJ, 6-Apr-2019.) (Proof shortened by AV, 1-Jul-2022.) Remove dependency on ax-10 2141, ax-11 2158, ax-12 2175, ax-un 7520. (Revised by Zhi Wang, 19-Sep-2024.) |
Ref | Expression |
---|---|
1oex | ⊢ 1o ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 8211 | . 2 ⊢ 1o = {∅} | |
2 | snex 5321 | . 2 ⊢ {∅} ∈ V | |
3 | 1, 2 | eqeltri 2834 | 1 ⊢ 1o ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 Vcvv 3405 ∅c0 4234 {csn 4538 1oc1o 8192 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 ax-sep 5189 ax-nul 5196 ax-pr 5319 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-tru 1546 df-fal 1556 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3407 df-dif 3866 df-un 3868 df-nul 4235 df-sn 4539 df-pr 4541 df-suc 6216 df-1o 8199 |
This theorem is referenced by: 2oexOLD 8217 oev 8238 oe0 8246 oev2 8247 oneo 8306 nnneo 8377 endisj 8729 map2xp 8813 sdom1 8875 1sdom 8878 djuexb 9522 djurcl 9524 djurf1o 9526 djuss 9533 djuun 9539 1stinr 9542 2ndinr 9543 pm54.43 9614 dju1dif 9783 djucomen 9788 djuassen 9789 infdju1 9800 pwdju1 9801 nnadju 9808 infmap2 9829 cfsuc 9868 isfin4p1 9926 dcomex 10058 pwcfsdom 10194 cfpwsdom 10195 canthp1lem2 10264 pwxpndom2 10276 indpi 10518 pinq 10538 archnq 10591 sadcf 16009 sadcp1 16011 fnpr2ob 17060 xpsfrnel 17064 xpsle 17081 setcepi 17591 setc2obas 17597 setc2ohom 17598 efgi1 19108 frgpuptinv 19158 dmdprdpr 19433 dprdpr 19434 coe1fval3 21126 00ply1bas 21158 ply1plusgfvi 21160 coe1z 21181 coe1tm 21191 xpstopnlem1 22703 xpstopnlem2 22705 xpsdsval 23276 fply1 31378 gonanegoal 33024 fmlaomn0 33062 gonan0 33064 gonarlem 33066 gonar 33067 fmlasucdisj 33071 satffunlem 33073 satffunlem2lem1 33076 ex-sategoelel12 33099 ssttrcl 33511 nofv 33594 noxp1o 33600 noextendlt 33606 bdayfo 33614 nosep1o 33618 nosepdmlem 33620 nolt02o 33632 nogt01o 33633 nosupbnd1lem5 33649 nosupbnd2lem1 33652 noinfno 33655 noinfbday 33657 noinfbnd1 33666 noinfbnd2lem1 33667 noinfbnd2 33668 noetasuplem1 33670 noetasuplem2 33671 noetasuplem4 33673 rankeq1o 34207 bj-pr2val 34942 bj-2upln1upl 34948 pw2f1ocnv 40560 clsk3nimkb 41325 clsk1indlem4 41329 clsk1indlem1 41330 f1omo 45859 f1omoALT 45860 indthinc 46004 indthincALT 46005 prsthinc 46006 prstchom 46027 prstchom2ALT 46029 |
Copyright terms: Public domain | W3C validator |