| 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 3355 | . . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)) | |
| 2 | 1 | simplbi 274 | . 2 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐵) → 𝑥 ∈ 𝐴) |
| 3 | 2 | ssriv 3196 | 1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2175 ∩ cin 3164 ⊆ wss 3165 |
| 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 1469 ax-7 1470 ax-gen 1471 ax-ie1 1515 ax-ie2 1516 ax-8 1526 ax-10 1527 ax-11 1528 ax-i12 1529 ax-bndl 1531 ax-4 1532 ax-17 1548 ax-i9 1552 ax-ial 1556 ax-i5r 1557 ax-ext 2186 |
| This theorem depends on definitions: df-bi 117 df-tru 1375 df-nf 1483 df-sb 1785 df-clab 2191 df-cleq 2197 df-clel 2200 df-nfc 2336 df-v 2773 df-in 3171 df-ss 3178 |
| This theorem is referenced by: inss2 3393 ssinss1 3401 unabs 3403 inssddif 3413 inv1 3496 disjdif 3532 inundifss 3537 relin1 4792 resss 4982 resmpt3 5007 cnvcnvss 5136 funin 5344 funimass2 5351 fnresin1 5389 fnres 5391 fresin 5453 ssimaex 5639 fneqeql2 5688 isoini2 5887 ofrfval 6166 ofvalg 6167 ofrval 6168 off 6170 ofres 6172 ofco 6176 smores 6377 smores2 6379 tfrlem5 6399 pmresg 6762 unfiin 7022 infidc 7035 sbthlem7 7064 peano5nnnn 8004 peano5nni 9038 rexanuz 11241 nninfdclemcl 12761 nninfdclemp1 12763 fvsetsid 12808 tgvalex 13037 tgval2 14465 eltg3 14471 tgcl 14478 tgdom 14486 tgidm 14488 epttop 14504 ntropn 14531 ntrin 14538 cnptopresti 14652 cnptoprest 14653 txcnmpt 14687 xmetres 14796 metres 14797 blin2 14846 metrest 14920 tgioo 14968 limcresi 15080 2sqlem8 15542 bj-charfun 15676 bj-charfundc 15677 bj-charfundcALT 15678 |
| Copyright terms: Public domain | W3C validator |