![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iinss | Structured version Visualization version GIF version |
Description: Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.) |
Ref | Expression |
---|---|
iinss | ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eliin 5003 | . . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) | |
2 | 1 | elv 3481 | . . 3 ⊢ (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
3 | ssel 3976 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | |
4 | 3 | reximi 3085 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
5 | r19.36v 3184 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | |
6 | 4, 5 | syl 17 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
7 | 2, 6 | biimtrid 241 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶)) |
8 | 7 | ssrdv 3989 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2107 ∀wral 3062 ∃wrex 3071 Vcvv 3475 ⊆ wss 3949 ∩ ciin 4999 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 df-rex 3072 df-v 3477 df-in 3956 df-ss 3966 df-iin 5001 |
This theorem is referenced by: riinn0 5087 reliin 5818 cnviin 6286 iiner 8783 scott0 9881 cfslb 10261 ptbasfi 23085 iscmet3 24810 fnemeet1 35251 pmapglb2N 38642 pmapglb2xN 38643 iinssd 43820 iooiinicc 44255 iooiinioc 44269 meaiininclem 45202 iinhoiicclem 45389 smflim 45493 smflimsuplem7 45542 |
Copyright terms: Public domain | W3C validator |