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

Theorem eliin 4915
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 2897 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 3194 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4913 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3665 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207   = wceq 1528  wcel 2105  wral 3135   ciin 4911
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-iin 4913
This theorem is referenced by:  iinconst  4920  iuniin  4922  iinssiun  4923  iinss1  4925  ssiinf  4969  iinss  4971  iinss2  4972  iinab  4981  iinun2  4986  iundif2  4987  iindif1  4988  iindif2  4990  iinin2  4991  elriin  4994  iinpw  5019  triin  5178  xpiindi  5699  cnviin  6130  iinpreima  6829  iiner  8358  ixpiin  8476  boxriin  8492  iunocv  20753  hauscmplem  21942  txtube  22176  isfcls  22545  iscmet3  23823  taylfval  24874  fnemeet1  33611  diaglbN  38071  dibglbN  38182  dihglbcpreN  38316  kelac1  39541  eliind  41210  eliuniin  41242  eliin2f  41247  eliinid  41254  eliuniin2  41263  iinssiin  41271  eliind2  41272  iinssf  41283  allbutfi  41541  meaiininclem  42645  hspdifhsp  42775  iinhoiicclem  42832  preimageiingt  42875  preimaleiinlt  42876  smflimlem2  42925  smflimsuplem5  42975  smflimsuplem7  42977
  Copyright terms: Public domain W3C validator