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

Theorem eliin 3910
Description: Membership in indexed intersection. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
eliin  |-  ( A  e.  V  ->  ( A  e.  |^|_ x  e.  B  C  <->  A. x  e.  B  A  e.  C ) )
Distinct variable group:    x, A
Allowed substitution hints:    B( x)    C( x)    V( x)

Proof of Theorem eliin
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 eleq1 2343 . . 3  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
21ralbidv 2563 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  C  <->  A. x  e.  B  A  e.  C ) )
3 df-iin 3908 . 2  |-  |^|_ x  e.  B  C  =  { y  |  A. x  e.  B  y  e.  C }
42, 3elab2g 2916 1  |-  ( A  e.  V  ->  ( A  e.  |^|_ x  e.  B  C  <->  A. x  e.  B  A  e.  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1623    e. wcel 1684   A.wral 2543   |^|_ciin 3906
This theorem is referenced by:  iinconst  3914  iuniin  3915  iinss1  3917  ssiinf  3951  iinss  3953  iinss2  3954  iinab  3963  iinun2  3968  iundif2  3969  iindif2  3971  iinin2  3972  elriin  3974  iinpw  3990  xpiindi  4821  cnviin  5212  iinpreima  5655  iiner  6731  ixpiin  6842  boxriin  6858  iunocv  16581  hauscmplem  17133  txtube  17334  isfcls  17704  iscmet3  18719  taylfval  19738  splint  25048  domintrefc  25125  dstr  25171  inttop2  25515  iintlem1  25610  iint  25612  fnemeet1  26315  kelac1  27161  diaglbN  31245  dibglbN  31356  dihglbcpreN  31490
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-iin 3908
  Copyright terms: Public domain W3C validator