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

Theorem eliin 4996
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 2829 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 3178 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4994 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3680 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206   = wceq 1540  wcel 2108  wral 3061   ciin 4992
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-iin 4994
This theorem is referenced by:  iinconst  5002  iuniin  5004  iinssiun  5005  iinss1  5007  ssiinf  5054  iinss  5056  iinss2  5057  iinab  5068  iinun2  5073  iundif2  5074  iindif1  5075  iindif2  5077  iinin2  5078  elriin  5081  iinpw  5106  triin  5276  xpiindi  5846  cnviin  6306  iinpreima  7089  iiner  8829  ixpiin  8964  boxriin  8980  iunocv  21699  hauscmplem  23414  txtube  23648  isfcls  24017  iscmet3  25327  taylfval  26400  zarclsiin  33870  fnemeet1  36367  diaglbN  41057  dibglbN  41168  dihglbcpreN  41302  kelac1  43075  eliind  45076  eliuniin  45104  eliin2f  45109  eliinid  45116  eliuniin2  45125  iinssiin  45134  eliind2  45135  iinssf  45143  iindif2f  45165  allbutfi  45404  meaiininclem  46501  hspdifhsp  46631  iinhoiicclem  46688  preimageiingt  46735  preimaleiinlt  46736  smflimlem2  46787  smflimsuplem5  46839  smflimsuplem7  46841
  Copyright terms: Public domain W3C validator