![]() |
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 5006 | . . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) | |
2 | 1 | elv 3468 | . . 3 ⊢ (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) |
3 | ssel 3973 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | |
4 | 3 | reximi 3074 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
5 | r19.36v 3174 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | |
6 | 4, 5 | syl 17 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) |
7 | 2, 6 | biimtrid 241 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶)) |
8 | 7 | ssrdv 3985 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∈ wcel 2099 ∀wral 3051 ∃wrex 3060 Vcvv 3462 ⊆ wss 3947 ∩ ciin 5002 |
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 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 df-rex 3061 df-v 3464 df-ss 3964 df-iin 5004 |
This theorem is referenced by: riinn0 5091 reliin 5823 cnviin 6297 iiner 8818 scott0 9929 cfslb 10309 ptbasfi 23576 iscmet3 25312 fnemeet1 36078 pmapglb2N 39470 pmapglb2xN 39471 iinssd 44732 iooiinicc 45160 iooiinioc 45174 meaiininclem 46107 iinhoiicclem 46294 smflim 46398 smflimsuplem7 46447 |
Copyright terms: Public domain | W3C validator |