![]() |
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 2700 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ V) | |
2 | 1 | ssriv 3106 | 1 ⊢ 𝐴 ⊆ V |
Colors of variables: wff set class |
Syntax hints: Vcvv 2689 ⊆ wss 3076 |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-v 2691 df-in 3082 df-ss 3089 |
This theorem is referenced by: ddifss 3319 inv1 3404 unv 3405 vss 3415 disj2 3423 pwv 3743 trv 4046 xpss 4655 djussxp 4692 dmv 4763 dmresi 4882 resid 4883 ssrnres 4989 rescnvcnv 5009 cocnvcnv1 5057 relrelss 5073 dffn2 5282 oprabss 5865 ofmres 6042 f1stres 6065 f2ndres 6066 fiintim 6825 djuf1olemr 6947 endjusym 6989 dju1p1e2 7070 suplocexprlemell 7545 seq3val 10262 seqvalcd 10263 seq3-1 10264 seqf 10265 seq3p1 10266 seqf2 10268 seq1cd 10269 seqp1cd 10270 setscom 12038 upxp 12480 uptx 12482 cnmptid 12489 cnmpt1st 12496 cnmpt2nd 12497 |
Copyright terms: Public domain | W3C validator |