Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ssv | 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 2723 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V) | |
2 | 1 | ssriv 3132 | 1 ⊢ 𝐴 ⊆ V |
Colors of variables: wff set class |
Syntax hints: Vcvv 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 3346 inv1 3431 unv 3432 vss 3442 disj2 3450 pwv 3773 trv 4077 xpss 4697 djussxp 4734 dmv 4805 dmresi 4924 resid 4925 ssrnres 5031 rescnvcnv 5051 cocnvcnv1 5099 relrelss 5115 dffn2 5324 oprabss 5910 ofmres 6087 f1stres 6110 f2ndres 6111 fiintim 6876 djuf1olemr 7001 endjusym 7043 dju1p1e2 7135 suplocexprlemell 7636 seq3val 10367 seqvalcd 10368 seq3-1 10369 seqf 10370 seq3p1 10371 seqf2 10373 seq1cd 10374 seqp1cd 10375 setscom 12326 upxp 12768 uptx 12770 cnmptid 12777 cnmpt1st 12784 cnmpt2nd 12785 |
Copyright terms: Public domain | W3C validator |