Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssv | 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 2723 | . 2 | |
2 | 1 | ssriv 3132 | 1 |
Colors of variables: wff set class |
Syntax hints: cvv 2712 wss 3102 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-11 1486 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-v 2714 df-in 3108 df-ss 3115 |
This theorem is referenced by: ddifss 3345 inv1 3430 unv 3431 vss 3441 disj2 3449 pwv 3772 trv 4075 xpss 4695 djussxp 4732 dmv 4803 dmresi 4922 resid 4923 ssrnres 5029 rescnvcnv 5049 cocnvcnv1 5097 relrelss 5113 dffn2 5322 oprabss 5908 ofmres 6085 f1stres 6108 f2ndres 6109 fiintim 6874 djuf1olemr 6999 endjusym 7041 dju1p1e2 7133 suplocexprlemell 7634 seq3val 10361 seqvalcd 10362 seq3-1 10363 seqf 10364 seq3p1 10365 seqf2 10367 seq1cd 10368 seqp1cd 10369 setscom 12272 upxp 12714 uptx 12716 cnmptid 12723 cnmpt1st 12730 cnmpt2nd 12731 |
Copyright terms: Public domain | W3C validator |