![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssv | Structured version Visualization version Unicode version |
Description: Any class is a subclass of the universal class. (Contributed by NM, 31-Oct-1995.) |
Ref | Expression |
---|---|
ssv |
![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elex 3056 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ssriv 3438 |
1
![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1671 ax-4 1684 ax-5 1760 ax-6 1807 ax-7 1853 ax-10 1917 ax-11 1922 ax-12 1935 ax-13 2093 ax-ext 2433 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1449 df-ex 1666 df-nf 1670 df-sb 1800 df-clab 2440 df-cleq 2446 df-clel 2449 df-v 3049 df-in 3413 df-ss 3420 |
This theorem is referenced by: inv1 3763 unv 3764 vss 3803 pssv 3806 disj2 3814 pwv 4200 unissint 4262 symdifv 4359 trv 4512 intabs 4567 xpss 4944 djussxp 4983 dmv 5053 dmresi 5163 resid 5165 ssrnres 5278 rescnvcnv 5301 cocnvcnv1 5349 relrelss 5362 dffn2 5735 oprabss 6387 fvresex 6771 ofmres 6794 f1stres 6820 f2ndres 6821 domssex2 7737 fineqv 7792 fiint 7853 marypha1lem 7952 marypha2 7958 cantnfval2 8179 oef1o 8208 dfac12lem2 8579 dfac12a 8583 fin23lem41 8787 dfacfin7 8834 iunfo 8969 gch2 9105 axpre-sup 9598 setscom 15165 isofn 15692 homaf 15937 dmaf 15956 cdaf 15957 prdsinvlem 16806 frgpuplem 17434 gsum2dlem2 17615 gsum2d 17616 mgpf 17804 prdsmgp 17850 prdscrngd 17853 pws1 17856 mulgass3 17877 crngridl 18474 ply1lss 18801 coe1fval3 18813 coe1tm 18878 ply1coe 18901 ply1coeOLD 18902 evl1expd 18945 frlmbas 19330 islindf3 19396 pmatcollpw3lem 19819 clscon 20457 ptbasfi 20608 upxp 20650 uptx 20652 prdstps 20656 hausdiag 20672 cnmptid 20688 cnmpt1st 20695 cnmpt2nd 20696 fbssint 20865 prdstmdd 21150 prdsxmslem2 21556 isngp2 21623 uniiccdif 22547 0vfval 26237 xppreima 28260 xppreima2 28261 1stpreimas 28298 ffsrn 28326 gsummpt2d 28556 qtophaus 28675 cnre2csqlem 28728 cntmeas 29060 eulerpartlemmf 29220 eulerpartlemgf 29224 sseqfv1 29234 sseqfn 29235 sseqfv2 29239 coinflippv 29328 erdszelem2 29927 mpstssv 30189 filnetlem4 31049 elxp8 31786 poimirlem16 31968 poimirlem19 31971 poimirlem20 31972 poimirlem26 31978 poimirlem27 31979 heibor1lem 32153 rmxyelqirr 35770 isnumbasgrplem1 35972 isnumbasgrplem2 35975 dfacbasgrp 35979 resnonrel 36210 comptiunov2i 36310 compne 36804 conss2 36807 |
Copyright terms: Public domain | W3C validator |