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 4167 | . . . . 5 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) | |
2 | 1 | imbi2i 338 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ (𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
3 | 2 | albii 1814 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))) |
4 | jcab 520 | . . . 4 ⊢ ((𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) | |
5 | 4 | albii 1814 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)) ↔ ∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
6 | 19.26 1865 | . . 3 ⊢ (∀𝑥((𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) | |
7 | 3, 5, 6 | 3bitrri 300 | . 2 ⊢ ((∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶))) |
8 | dfss2 3953 | . . 3 ⊢ (𝐴 ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)) | |
9 | dfss2 3953 | . . 3 ⊢ (𝐴 ⊆ 𝐶 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶)) | |
10 | 8, 9 | anbi12i 628 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ (∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵) ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐶))) |
11 | dfss2 3953 | . 2 ⊢ (𝐴 ⊆ (𝐵 ∩ 𝐶) ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝑥 ∈ (𝐵 ∩ 𝐶))) | |
12 | 7, 10, 11 | 3bitr4i 305 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∀wal 1529 ∈ wcel 2108 ∩ cin 3933 ⊆ wss 3934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-v 3495 df-in 3941 df-ss 3950 |
This theorem is referenced by: ssini 4206 ssind 4207 uneqin 4253 disjpss 4408 trin 5173 pwin 5445 fin 6552 wfrlem4 7950 epfrs 9165 tcmin 9175 resscntz 18454 subgdmdprd 19148 tgval 21555 eltg3i 21561 innei 21725 cnprest2 21890 subislly 22081 lly1stc 22096 xkohaus 22253 xkoinjcn 22287 opnfbas 22442 supfil 22495 rnelfm 22553 tsmsres 22744 restmetu 23172 chabs2 29286 cmbr4i 29370 pjin3i 29963 mdbr2 30065 dmdbr2 30072 dmdbr5 30077 mdslle1i 30086 mdslle2i 30087 mdslj1i 30088 mdslj2i 30089 mdsl2i 30091 mdslmd1lem1 30094 mdslmd1lem2 30095 mdslmd1i 30098 mdslmd3i 30101 hatomistici 30131 chrelat2i 30134 cvexchlem 30137 mdsymlem1 30172 mdsymlem3 30174 mdsymlem6 30177 dmdbr5ati 30191 pnfneige0 31187 ballotlem2 31739 iccllysconn 32490 frrlem4 33119 frrlem13 33128 heibor1lem 35079 dochexmidlem1 38588 superficl 39917 k0004lem1 40488 |
Copyright terms: Public domain | W3C validator |