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

Theorem eliin 4034
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 2441 . . 3  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
21ralbidv 2663 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  C  <->  A. x  e.  B  A  e.  C ) )
3 df-iin 4032 . 2  |-  |^|_ x  e.  B  C  =  { y  |  A. x  e.  B  y  e.  C }
42, 3elab2g 3021 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 177    = wceq 1649    e. wcel 1717   A.wral 2643   |^|_ciin 4030
This theorem is referenced by:  iinconst  4038  iuniin  4039  iinss1  4041  ssiinf  4075  iinss  4077  iinss2  4078  iinab  4087  iinun2  4092  iundif2  4093  iindif2  4095  iinin2  4096  elriin  4098  iinpw  4114  xpiindi  4944  cnviin  5343  iinpreima  5793  iiner  6906  ixpiin  7018  boxriin  7034  iunocv  16825  hauscmplem  17385  txtube  17587  isfcls  17956  iscmet3  19111  taylfval  20136  fnemeet1  26080  kelac1  26824  diaglbN  31222  dibglbN  31333  dihglbcpreN  31467
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2362
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2506  df-ral 2648  df-v 2895  df-iin 4032
  Copyright terms: Public domain W3C validator