![]() |
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.) |
Ref | Expression |
---|---|
1oex | ⊢ 1o ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1on 7967 | . 2 ⊢ 1o ∈ On | |
2 | 1 | elexi 3459 | 1 ⊢ 1o ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2083 Vcvv 3440 Oncon0 6073 1oc1o 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 |
Copyright terms: Public domain | W3C validator |