Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > inss2 | 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 |
---|---|
inss2 | ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | incom 3263 | . 2 ⊢ (𝐵 ∩ 𝐴) = (𝐴 ∩ 𝐵) | |
2 | inss1 3291 | . 2 ⊢ (𝐵 ∩ 𝐴) ⊆ 𝐵 | |
3 | 1, 2 | eqsstrri 3125 | 1 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵 |
Colors of variables: wff set class |
Syntax hints: ∩ cin 3065 ⊆ wss 3066 |
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-io 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2119 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2124 df-cleq 2130 df-clel 2133 df-nfc 2268 df-v 2683 df-in 3072 df-ss 3079 |
This theorem is referenced by: difin0 3431 bnd2 4092 ordin 4302 relin2 4653 relres 4842 ssrnres 4976 cnvcnv 4986 funinsn 5167 funimaexg 5202 fnresin2 5233 ssimaex 5475 ffvresb 5576 ofrfval 5983 ofvalg 5984 ofrval 5985 off 5987 ofres 5989 ofco 5993 offres 6026 tpostpos 6154 smores3 6183 tfrlem5 6204 tfrexlem 6224 erinxp 6496 pmresg 6563 unfiin 6807 ltrelpi 7125 peano5nnnn 7693 peano5nni 8716 rexanuz 10753 structcnvcnv 11964 restsspw 12119 eltg4i 12213 ntrss2 12279 ntrin 12282 isopn3 12283 resttopon 12329 restuni2 12335 cnrest2r 12395 cnptopresti 12396 cnptoprest 12397 lmss 12404 metrest 12664 tgioo 12704 peano5set 13127 |
Copyright terms: Public domain | W3C validator |