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

Theorem eliin 4557
 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 2718 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 3015 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4555 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3385 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∩ ciin 4553 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-v 3233  df-iin 4555 This theorem is referenced by:  iinconst  4562  iuniin  4563  iinss1  4565  ssiinf  4601  iinss  4603  iinss2  4604  iinab  4613  iinun2  4618  iundif2  4619  iindif2  4621  iinin2  4622  elriin  4625  iinpw  4649  xpiindi  5290  cnviin  5710  iinpreima  6385  iiner  7862  ixpiin  7976  boxriin  7992  iunocv  20073  hauscmplem  21257  txtube  21491  isfcls  21860  iscmet3  23137  taylfval  24158  iinssiun  29503  fnemeet1  32486  diaglbN  36661  dibglbN  36772  dihglbcpreN  36906  kelac1  37950  eliind  39554  eliuniin  39593  eliin2f  39601  eliinid  39608  eliuniin2  39617  iinssiin  39626  eliind2  39627  iinssf  39641  allbutfi  39929  meaiininclem  41021  hspdifhsp  41151  iinhoiicclem  41208  preimageiingt  41251  preimaleiinlt  41252  smflimlem2  41301  smflimsuplem5  41351  smflimsuplem7  41353
 Copyright terms: Public domain W3C validator