Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssv | Structured version Visualization version GIF version |
Description: Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.) |
Ref | Expression |
---|---|
ssv | ⊢ 𝐴 ⊆ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3510 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V) | |
2 | 1 | ssriv 3968 | 1 ⊢ 𝐴 ⊆ V |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3492 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-v 3494 df-in 3940 df-ss 3949 |
This theorem is referenced by: inv1 4345 unv 4346 vss 4391 pssv 4394 disj2 4403 pwv 4827 unissint 4891 symdifv 4999 trv 5175 intabs 5236 xpss 5564 inxpssres 5565 djussxp 5709 dmv 5785 dmresi 5914 cnvrescnv 6045 rescnvcnv 6054 cocnvcnv1 6103 relrelss 6117 fnresi 6469 dffn2 6509 oprabss 7249 fvresex 7650 ofmres 7674 f1stres 7702 f2ndres 7703 fsplitfpar 7803 domssex2 8665 fineqv 8721 fiint 8783 marypha1lem 8885 marypha2 8891 cantnfval2 9120 inlresf1 9332 inrresf1 9334 djuun 9343 dfac12lem2 9558 dfac12a 9562 fin23lem41 9762 dfacfin7 9809 iunfo 9949 gch2 10085 axpre-sup 10579 wrdv 13865 wrdvOLD 13866 setscom 16515 isofn 17033 homaf 17278 dmaf 17297 cdaf 17298 prdsinvlem 18146 frgpuplem 18827 gsum2dlem2 19020 gsum2d 19021 mgpf 19238 prdsmgp 19289 prdscrngd 19292 pws1 19295 mulgass3 19316 crngridl 19939 ply1lss 20292 coe1fval3 20304 coe1tm 20369 ply1coe 20392 evl1expd 20436 frlmbas 20827 islindf3 20898 pmatcollpw3lem 21319 clsconn 21966 ptbasfi 22117 upxp 22159 uptx 22161 prdstps 22165 hausdiag 22181 cnmpt1st 22204 cnmpt2nd 22205 fbssint 22374 prdstmdd 22659 prdsxmslem2 23066 isngp2 23133 uniiccdif 24106 wlkdlem1 27391 0vfval 28310 xppreima 30322 xppreima2 30323 1stpreimas 30367 fsuppcurry1 30387 fsuppcurry2 30388 ffsrn 30391 gsummpt2d 30614 lindflbs 30867 dimval 30900 dimvalfi 30901 qtophaus 30999 cnre2csqlem 31052 cntmeas 31384 eulerpartlemmf 31532 eulerpartlemgf 31536 sseqfv1 31546 sseqfn 31547 sseqfv2 31551 coinflippv 31640 erdszelem2 32336 mpstssv 32683 filnetlem4 33626 bj-0int 34287 bj-idres 34344 elxp8 34534 poimirlem16 34789 poimirlem19 34792 poimirlem20 34793 poimirlem26 34799 poimirlem27 34800 heibor1lem 34968 rmxyelqirr 39385 isnumbasgrplem1 39579 isnumbasgrplem2 39582 dfacbasgrp 39586 resnonrel 39830 comptiunov2i 39929 ntrneiel2 40314 ntrneik4w 40328 conss2 40652 |
Copyright terms: Public domain | W3C validator |