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

Theorem eliin 4090
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 2495 . . 3  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
21ralbidv 2717 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  C  <->  A. x  e.  B  A  e.  C ) )
3 df-iin 4088 . 2  |-  |^|_ x  e.  B  C  =  { y  |  A. x  e.  B  y  e.  C }
42, 3elab2g 3076 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 1652    e. wcel 1725   A.wral 2697   |^|_ciin 4086
This theorem is referenced by:  iinconst  4094  iuniin  4095  iinss1  4097  ssiinf  4132  iinss  4134  iinss2  4135  iinab  4144  iinun2  4149  iundif2  4150  iindif2  4152  iinin2  4153  elriin  4155  iinpw  4171  xpiindi  5002  cnviin  5401  iinpreima  5852  iiner  6968  ixpiin  7080  boxriin  7096  iunocv  16900  hauscmplem  17461  txtube  17664  isfcls  18033  iscmet3  19238  taylfval  20267  fnemeet1  26386  kelac1  27129  diaglbN  31790  dibglbN  31901  dihglbcpreN  32035
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-v 2950  df-iin 4088
  Copyright terms: Public domain W3C validator