MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  iinss Structured version   Visualization version   GIF version

Theorem iinss 4804
Description: Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003.) (Proof shortened by Andrew Salmon, 25-Jul-2011.)
Assertion
Ref Expression
iinss (∃𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵𝐶)
Distinct variable group:   𝑥,𝐶
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem iinss
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eliin 4758 . . . 4 (𝑦 ∈ V → (𝑦 𝑥𝐴 𝐵 ↔ ∀𝑥𝐴 𝑦𝐵))
21elv 3401 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∀𝑥𝐴 𝑦𝐵)
3 ssel 3814 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
43reximi 3191 . . . 4 (∃𝑥𝐴 𝐵𝐶 → ∃𝑥𝐴 (𝑦𝐵𝑦𝐶))
5 r19.36v 3270 . . . 4 (∃𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∀𝑥𝐴 𝑦𝐵𝑦𝐶))
64, 5syl 17 . . 3 (∃𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 𝑦𝐵𝑦𝐶))
72, 6syl5bi 234 . 2 (∃𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦𝐶))
87ssrdv 3826 1 (∃𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wcel 2106  wral 3089  wrex 3090  Vcvv 3397  wss 3791   ciin 4754
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-ext 2753
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ral 3094  df-rex 3095  df-v 3399  df-in 3798  df-ss 3805  df-iin 4756
This theorem is referenced by:  riinn0  4828  reliin  5488  cnviin  5926  iiner  8102  scott0  9046  cfslb  9423  ptbasfi  21793  iscmet3  23499  fnemeet1  32963  pmapglb2N  35919  pmapglb2xN  35920  iinssd  40234  iooiinicc  40669  iooiinioc  40683  meaiininclem  41619  iinhoiicclem  41806  smflim  41904  smflimsuplem7  41951
  Copyright terms: Public domain W3C validator