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

Theorem eliin 4923
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 2826 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 3119 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4921 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3601 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209   = wceq 1543  wcel 2111  wral 3062   ciin 4919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3067  df-iin 4921
This theorem is referenced by:  iinconst  4928  iuniin  4930  iinssiun  4931  iinss1  4933  ssiinf  4977  iinss  4979  iinss2  4980  iinab  4990  iinun2  4995  iundif2  4996  iindif1  4997  iindif2  4999  iinin2  5000  elriin  5003  iinpw  5028  triin  5190  xpiindi  5718  cnviin  6163  iinpreima  6907  iiner  8491  ixpiin  8625  boxriin  8641  iunocv  20667  hauscmplem  22327  txtube  22561  isfcls  22930  iscmet3  24214  taylfval  25275  zarclsiin  31559  fnemeet1  34318  diaglbN  38832  dibglbN  38943  dihglbcpreN  39077  kelac1  40619  eliind  42320  eliuniin  42350  eliin2f  42355  eliinid  42362  eliuniin2  42370  iinssiin  42379  eliind2  42380  iinssf  42388  allbutfi  42634  meaiininclem  43727  hspdifhsp  43857  iinhoiicclem  43914  preimageiingt  43957  preimaleiinlt  43958  smflimlem2  44007  smflimsuplem5  44057  smflimsuplem7  44059
  Copyright terms: Public domain W3C validator