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

Theorem iinss 5055
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 4995 . . . 4 (𝑦 ∈ V → (𝑦 𝑥𝐴 𝐵 ↔ ∀𝑥𝐴 𝑦𝐵))
21elv 3484 . . 3 (𝑦 𝑥𝐴 𝐵 ↔ ∀𝑥𝐴 𝑦𝐵)
3 ssel 3976 . . . . 5 (𝐵𝐶 → (𝑦𝐵𝑦𝐶))
43reximi 3083 . . . 4 (∃𝑥𝐴 𝐵𝐶 → ∃𝑥𝐴 (𝑦𝐵𝑦𝐶))
5 r19.36v 3183 . . . 4 (∃𝑥𝐴 (𝑦𝐵𝑦𝐶) → (∀𝑥𝐴 𝑦𝐵𝑦𝐶))
64, 5syl 17 . . 3 (∃𝑥𝐴 𝐵𝐶 → (∀𝑥𝐴 𝑦𝐵𝑦𝐶))
72, 6biimtrid 242 . 2 (∃𝑥𝐴 𝐵𝐶 → (𝑦 𝑥𝐴 𝐵𝑦𝐶))
87ssrdv 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