|   | 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 4995 | . . . 4 ⊢ (𝑦 ∈ V → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵)) | |
| 2 | 1 | elv 3484 | . . 3 ⊢ (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 ↔ ∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵) | 
| 3 | ssel 3976 | . . . . 5 ⊢ (𝐵 ⊆ 𝐶 → (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | |
| 4 | 3 | reximi 3083 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | 
| 5 | r19.36v 3183 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 (𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶) → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | |
| 6 | 4, 5 | syl 17 | . . 3 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (∀𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 → 𝑦 ∈ 𝐶)) | 
| 7 | 2, 6 | biimtrid 242 | . 2 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → (𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ 𝐶)) | 
| 8 | 7 | ssrdv 3988 | 1 ⊢ (∃𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶 → ∩ 𝑥 ∈ 𝐴 𝐵 ⊆ 𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∈ wcel 2107 ∀wral 3060 ∃wrex 3069 Vcvv 3479 ⊆ wss 3950 ∩ ciin 4991 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-rex 3070 df-v 3481 df-ss 3967 df-iin 4993 | 
| This theorem is referenced by: riinn0 5082 reliin 5826 cnviin 6305 iiner 8830 scott0 9927 cfslb 10307 ptbasfi 23590 iscmet3 25328 fnemeet1 36368 pmapglb2N 39774 pmapglb2xN 39775 iinssd 45141 iooiinicc 45560 iooiinioc 45574 meaiininclem 46506 iinhoiicclem 46693 smflim 46797 smflimsuplem7 46846 | 
| Copyright terms: Public domain | W3C validator |