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 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  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  8724  ixpiin  8858  boxriin  8874  iunocv  21070  hauscmplem  22741  txtube  22975  isfcls  23344  iscmet3  24641  taylfval  25702  zarclsiin  32321  fnemeet1  34805  diaglbN  39485  dibglbN  39596  dihglbcpreN  39730  kelac1  41328  eliind  43221  eliuniin  43251  eliin2f  43256  eliinid  43263  eliuniin2  43272  iinssiin  43281  eliind2  43282  iinssf  43290  iindif2f  43317  allbutfi  43564  meaiininclem  44659  hspdifhsp  44789  iinhoiicclem  44846  preimageiingt  44893  preimaleiinlt  44894  smflimlem2  44945  smflimsuplem5  44997  smflimsuplem7  44999
  Copyright terms: Public domain W3C validator