![]() |
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 3243 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V) | |
2 | 1 | ssriv 3640 | 1 ⊢ 𝐴 ⊆ V |
Colors of variables: wff setvar class |
Syntax hints: Vcvv 3231 ⊆ wss 3607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-v 3233 df-in 3614 df-ss 3621 |
This theorem is referenced by: inv1 4003 unv 4004 vss 4045 pssv 4049 disj2 4057 pwv 4465 unissint 4533 symdifv 4630 trv 4798 intabs 4855 xpss 5159 djussxp 5300 dmv 5373 dmresi 5492 residOLD 5495 ssrnres 5607 rescnvcnv 5632 cocnvcnv1 5684 relrelss 5697 dffn2 6085 oprabss 6788 fvresex 7181 ofmres 7206 f1stres 7234 f2ndres 7235 domssex2 8161 fineqv 8216 fiint 8278 marypha1lem 8380 marypha2 8386 cantnfval2 8604 oef1o 8633 dfac12lem2 9004 dfac12a 9008 fin23lem41 9212 dfacfin7 9259 iunfo 9399 gch2 9535 axpre-sup 10028 wrdv 13352 setscom 15950 isofn 16482 homaf 16727 dmaf 16746 cdaf 16747 prdsinvlem 17571 frgpuplem 18231 gsum2dlem2 18416 gsum2d 18417 mgpf 18605 prdsmgp 18656 prdscrngd 18659 pws1 18662 mulgass3 18683 crngridl 19286 ply1lss 19614 coe1fval3 19626 coe1tm 19691 ply1coe 19714 evl1expd 19757 frlmbas 20147 islindf3 20213 pmatcollpw3lem 20636 clsconn 21281 ptbasfi 21432 upxp 21474 uptx 21476 prdstps 21480 hausdiag 21496 cnmptid 21512 cnmpt1st 21519 cnmpt2nd 21520 fbssint 21689 prdstmdd 21974 prdsxmslem2 22381 isngp2 22448 uniiccdif 23392 wlkdlem1 26635 0vfval 27589 xppreima 29577 xppreima2 29578 1stpreimas 29611 ffsrn 29632 gsummpt2d 29909 qtophaus 30031 cnre2csqlem 30084 cntmeas 30417 eulerpartlemmf 30565 eulerpartlemgf 30569 sseqfv1 30579 sseqfn 30580 sseqfv2 30584 coinflippv 30673 erdszelem2 31300 mpstssv 31562 filnetlem4 32501 bj-0int 33180 elxp8 33349 poimirlem16 33555 poimirlem19 33558 poimirlem20 33559 poimirlem26 33565 poimirlem27 33566 heibor1lem 33738 inxpssres 34217 rmxyelqirr 37792 isnumbasgrplem1 37988 isnumbasgrplem2 37991 dfacbasgrp 37995 resnonrel 38215 comptiunov2i 38315 ntrneiel2 38701 ntrneik4w 38715 compneOLD 38961 conss2 38964 |
Copyright terms: Public domain | W3C validator |