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

Theorem eliin 3926
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 2356 . . 3  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
21ralbidv 2576 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  C  <->  A. x  e.  B  A  e.  C ) )
3 df-iin 3924 . 2  |-  |^|_ x  e.  B  C  =  { y  |  A. x  e.  B  y  e.  C }
42, 3elab2g 2929 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 1632    e. wcel 1696   A.wral 2556   |^|_ciin 3922
This theorem is referenced by:  iinconst  3930  iuniin  3931  iinss1  3933  ssiinf  3967  iinss  3969  iinss2  3970  iinab  3979  iinun2  3984  iundif2  3985  iindif2  3987  iinin2  3988  elriin  3990  iinpw  4006  xpiindi  4837  cnviin  5228  iinpreima  5671  iiner  6747  ixpiin  6858  boxriin  6874  iunocv  16597  hauscmplem  17149  txtube  17350  isfcls  17720  iscmet3  18735  taylfval  19754  splint  25151  domintrefc  25228  dstr  25274  inttop2  25618  iintlem1  25713  iint  25715  fnemeet1  26418  kelac1  27264  diaglbN  31867  dibglbN  31978  dihglbcpreN  32112
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-v 2803  df-iin 3924
  Copyright terms: Public domain W3C validator