![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > inss1 | GIF version |
Description: The intersection of two classes is a subset of one of them. Part of Exercise 12 of [TakeutiZaring] p. 18. (Contributed by NM, 27-Apr-1994.) |
Ref | Expression |
---|---|
inss1 | ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3333 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
2 | 1 | simplbi 274 | . 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → 𝑥 ∈ 𝐴) |
3 | 2 | ssriv 3174 | 1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 ∩ cin 3143 ⊆ wss 3144 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-in 3150 df-ss 3157 |
This theorem is referenced by: inss2 3371 ssinss1 3379 unabs 3381 inssddif 3391 inv1 3474 disjdif 3510 inundifss 3515 relin1 4762 resss 4949 resmpt3 4974 cnvcnvss 5101 funin 5306 funimass2 5313 fnresin1 5349 fnres 5351 fresin 5413 ssimaex 5598 fneqeql2 5646 isoini2 5841 ofrfval 6116 ofvalg 6117 ofrval 6118 off 6120 ofres 6122 ofco 6126 smores 6318 smores2 6320 tfrlem5 6340 pmresg 6703 unfiin 6955 infidc 6965 sbthlem7 6993 peano5nnnn 7922 peano5nni 8953 rexanuz 11032 nninfdclemcl 12502 nninfdclemp1 12504 fvsetsid 12549 tgvalex 12771 tgval2 14028 eltg3 14034 tgcl 14041 tgdom 14049 tgidm 14051 epttop 14067 ntropn 14094 ntrin 14101 cnptopresti 14215 cnptoprest 14216 txcnmpt 14250 xmetres 14359 metres 14360 blin2 14409 metrest 14483 tgioo 14523 limcresi 14612 2sqlem8 14948 bj-charfun 15037 bj-charfundc 15038 bj-charfundcALT 15039 |
Copyright terms: Public domain | W3C validator |