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

Theorem eliin 4957
Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
eliin (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
Distinct variable group:   𝑥,𝐴
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑥)   𝑉(𝑥)

Proof of Theorem eliin
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eleq1 2825 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 3172 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4955 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3630 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1541  wcel 2106  wral 3062   ciin 4953
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-ral 3063  df-iin 4955
This theorem is referenced by:  iinconst  4962  iuniin  4964  iinssiun  4965  iinss1  4967  ssiinf  5012  iinss  5014  iinss2  5015  iinab  5026  iinun2  5031  iundif2  5032  iindif1  5033  iindif2  5035  iinin2  5036  elriin  5039  iinpw  5064  triin  5237  xpiindi  5789  cnviin  6236  iinpreima  7016  iiner  8686  ixpiin  8820  boxriin  8836  iunocv  21038  hauscmplem  22709  txtube  22943  isfcls  23312  iscmet3  24609  taylfval  25670  zarclsiin  32264  fnemeet1  34776  diaglbN  39456  dibglbN  39567  dihglbcpreN  39701  kelac1  41299  eliind  43190  eliuniin  43220  eliin2f  43225  eliinid  43232  eliuniin2  43241  iinssiin  43250  eliind2  43251  iinssf  43259  iindif2f  43286  allbutfi  43533  meaiininclem  44628  hspdifhsp  44758  iinhoiicclem  44815  preimageiingt  44862  preimaleiinlt  44863  smflimlem2  44914  smflimsuplem5  44966  smflimsuplem7  44968
  Copyright terms: Public domain W3C validator