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

Theorem eliin 4455
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 2675 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 2968 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4452 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3321 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194   = wceq 1474  wcel 1976  wral 2895   ciin 4450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-v 3174  df-iin 4452
This theorem is referenced by:  iinconst  4460  iuniin  4461  iinss1  4463  ssiinf  4499  iinss  4501  iinss2  4502  iinab  4511  iinun2  4516  iundif2  4517  iindif2  4519  iinin2  4520  elriin  4523  iinpw  4544  xpiindi  5167  cnviin  5575  iinpreima  6238  iiner  7683  ixpiin  7797  boxriin  7813  iunocv  19786  hauscmplem  20961  txtube  21195  isfcls  21565  iscmet3  22817  taylfval  23834  fnemeet1  31337  diaglbN  35165  dibglbN  35276  dihglbcpreN  35410  kelac1  36454  eliind  38069  eliuniin  38110  eliin2f  38119  eliinid  38128  eliuniin2  38138  allbutfi  38361  meaiininclem  39180  hspdifhsp  39310  iinhoiicclem  39368  preimageiingt  39411  preimaleiinlt  39412  smflimlem2  39462
  Copyright terms: Public domain W3C validator