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

Theorem iinss 4955
 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 4899 . . . 4 (𝑦 ∈ V → (𝑦 𝑥𝐴 𝐵 ↔ ∀𝑥𝐴 𝑦𝐵))
21elv 3474 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∀𝑥𝐴 𝑦𝐵)
3 ssel 3935 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
43reximi 3231 . . . 4 (∃𝑥𝐴 𝐵𝐶 → ∃𝑥𝐴 (𝑦𝐵𝑦𝐶))
5 r19.36v 3324 . . . 4 (∃𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∀𝑥𝐴 𝑦𝐵𝑦𝐶))
64, 5syl 17 . . 3 (∃𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 𝑦𝐵𝑦𝐶))
72, 6syl5bi 245 . 2 (∃𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦𝐶))
87ssrdv 3948 1 (∃𝑥𝐴 𝐵𝐶 𝑥𝐴 𝐵𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2114  ∀wral 3130  ∃wrex 3131  Vcvv 3469   ⊆ wss 3908  ∩ ciin 4895 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ral 3135  df-rex 3136  df-v 3471  df-in 3915  df-ss 3925  df-iin 4897 This theorem is referenced by:  riinn0  4980  reliin  5667  cnviin  6115  iiner  8356  scott0  9303  cfslb  9677  ptbasfi  22184  iscmet3  23895  fnemeet1  33788  pmapglb2N  37025  pmapglb2xN  37026  iinssd  41702  iooiinicc  42118  iooiinioc  42132  meaiininclem  43064  iinhoiicclem  43251  smflim  43349  smflimsuplem7  43396
 Copyright terms: Public domain W3C validator