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

Theorem eliin 4760
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 2847 . . 3 (𝑦 = 𝐴 → (𝑦𝐶𝐴𝐶))
21ralbidv 3168 . 2 (𝑦 = 𝐴 → (∀𝑥𝐵 𝑦𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
3 df-iin 4758 . 2 𝑥𝐵 𝐶 = {𝑦 ∣ ∀𝑥𝐵 𝑦𝐶}
42, 3elab2g 3561 1 (𝐴𝑉 → (𝐴 𝑥𝐵 𝐶 ↔ ∀𝑥𝐵 𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198   = wceq 1601  wcel 2107  wral 3090   ciin 4756
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ral 3095  df-v 3400  df-iin 4758
This theorem is referenced by:  iinconst  4765  iuniin  4766  iinss1  4768  ssiinf  4804  iinss  4806  iinss2  4807  iinab  4816  iinun2  4821  iundif2  4822  iindif2  4824  iinin2  4825  elriin  4828  iinpw  4853  triin  5004  xpiindi  5505  cnviin  5928  iinpreima  6611  iiner  8104  ixpiin  8222  boxriin  8238  iunocv  20435  hauscmplem  21629  txtube  21863  isfcls  22232  iscmet3  23510  taylfval  24561  iinssiun  29956  fnemeet1  32957  diaglbN  37218  dibglbN  37329  dihglbcpreN  37463  kelac1  38606  eliind  40185  eliuniin  40224  eliin2f  40230  eliinid  40237  eliuniin2  40246  iinssiin  40254  eliind2  40255  iinssf  40267  allbutfi  40536  meaiininclem  41641  hspdifhsp  41771  iinhoiicclem  41828  preimageiingt  41871  preimaleiinlt  41872  smflimlem2  41921  smflimsuplem5  41971  smflimsuplem7  41973
  Copyright terms: Public domain W3C validator