![]() |
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 3040 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ssriv 3422 |
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 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-v 3033 df-in 3397 df-ss 3404 |
This theorem is referenced by: inv1 3764 unv 3765 vss 3805 pssv 3808 disj2 3816 pwv 4189 unissint 4250 symdifv 4347 trv 4502 intabs 4562 xpss 4946 djussxp 4985 dmv 5056 dmresi 5166 resid 5168 ssrnres 5281 rescnvcnv 5305 cocnvcnv1 5353 relrelss 5366 dffn2 5741 oprabss 6401 fvresex 6785 ofmres 6808 f1stres 6834 f2ndres 6835 domssex2 7750 fineqv 7805 fiint 7866 marypha1lem 7965 marypha2 7971 cantnfval2 8192 oef1o 8221 dfac12lem2 8592 dfac12a 8596 fin23lem41 8800 dfacfin7 8847 iunfo 8982 gch2 9118 axpre-sup 9611 wrdv 12733 setscom 15231 isofn 15758 homaf 16003 dmaf 16022 cdaf 16023 prdsinvlem 16872 frgpuplem 17500 gsum2dlem2 17681 gsum2d 17682 mgpf 17870 prdsmgp 17916 prdscrngd 17919 pws1 17922 mulgass3 17943 crngridl 18539 ply1lss 18866 coe1fval3 18878 coe1tm 18943 ply1coe 18966 ply1coeOLD 18967 evl1expd 19010 frlmbas 19395 islindf3 19461 pmatcollpw3lem 19884 clscon 20522 ptbasfi 20673 upxp 20715 uptx 20717 prdstps 20721 hausdiag 20737 cnmptid 20753 cnmpt1st 20760 cnmpt2nd 20761 fbssint 20931 prdstmdd 21216 prdsxmslem2 21622 isngp2 21689 uniiccdif 22614 0vfval 26306 xppreima 28324 xppreima2 28325 1stpreimas 28361 ffsrn 28389 gsummpt2d 28618 qtophaus 28737 cnre2csqlem 28790 cntmeas 29122 eulerpartlemmf 29281 eulerpartlemgf 29285 sseqfv1 29295 sseqfn 29296 sseqfv2 29300 coinflippv 29389 erdszelem2 29987 mpstssv 30249 filnetlem4 31108 elxp8 31844 poimirlem16 32020 poimirlem19 32023 poimirlem20 32024 poimirlem26 32030 poimirlem27 32031 heibor1lem 32205 rmxyelqirr 35829 isnumbasgrplem1 36031 isnumbasgrplem2 36034 dfacbasgrp 36038 resnonrel 36269 comptiunov2i 36369 compne 36863 conss2 36866 1wlkdlem1 39882 |
Copyright terms: Public domain | W3C validator |