![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssin | Structured version Visualization version GIF version |
Description: Subclass of intersection. Theorem 2.8(vii) of [Monk1] p. 26. (Contributed by NM, 15-Jun-2004.) (Proof shortened by Andrew Salmon, 26-Jun-2011.) |
Ref | Expression |
---|---|
ssin | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elin 3978 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
2 | 1 | imbi2i 336 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
3 | 2 | albii 1815 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
4 | jcab 517 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) | |
5 | 4 | albii 1815 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
6 | 19.26 1867 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) | |
7 | 3, 5, 6 | 3bitrri 298 | . 2 ⊢ ((∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶))) |
8 | df-ss 3979 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
9 | df-ss 3979 | . . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
10 | 8, 9 | anbi12i 628 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
11 | df-ss 3979 | . 2 ⊢ (𝐴 ⊆ (𝐵 ∩ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶))) | |
12 | 7, 10, 11 | 3bitr4i 303 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∀wal 1534 ∈ wcel 2105 ∩ cin 3961 ⊆ wss 3962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-ext 2705 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1539 df-ex 1776 df-sb 2062 df-clab 2712 df-cleq 2726 df-clel 2813 df-v 3479 df-in 3969 df-ss 3979 |
This theorem is referenced by: ssini 4247 ssind 4248 uneqin 4294 disjpss 4466 trin 5276 pwin 5578 fin 6788 frrlem4 8312 frrlem13 8321 wfrlem4OLD 8350 epfrs 9768 tcmin 9778 resscntz 19363 subgdmdprd 20068 tgval 22977 eltg3i 22983 innei 23148 cnprest2 23313 subislly 23504 lly1stc 23519 xkohaus 23676 xkoinjcn 23710 opnfbas 23865 supfil 23918 rnelfm 23976 tsmsres 24167 restmetu 24598 chabs2 31545 cmbr4i 31629 pjin3i 32222 mdbr2 32324 dmdbr2 32331 dmdbr5 32336 mdslle1i 32345 mdslle2i 32346 mdslj1i 32347 mdslj2i 32348 mdsl2i 32350 mdslmd1lem1 32353 mdslmd1lem2 32354 mdslmd1i 32357 mdslmd3i 32360 hatomistici 32390 chrelat2i 32393 cvexchlem 32396 mdsymlem1 32431 mdsymlem3 32433 mdsymlem6 32436 dmdbr5ati 32450 pnfneige0 33911 ballotlem2 34469 iccllysconn 35234 heibor1lem 37795 relssinxpdmrn 38330 dochexmidlem1 41442 superficl 43556 k0004lem1 44136 ismnushort 44296 |
Copyright terms: Public domain | W3C validator |