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

Theorem eliin 4321
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 2515 . . 3  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
21ralbidv 2882 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  C  <->  A. x  e.  B  A  e.  C ) )
3 df-iin 4318 . 2  |-  |^|_ x  e.  B  C  =  { y  |  A. x  e.  B  y  e.  C }
42, 3elab2g 3234 1  |-  ( A  e.  V  ->  ( A  e.  |^|_ x  e.  B  C  <->  A. x  e.  B  A  e.  C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1383    e. wcel 1804   A.wral 2793   |^|_ciin 4316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097  df-iin 4318
This theorem is referenced by:  iinconst  4325  iuniin  4326  iinss1  4328  ssiinf  4364  iinss  4366  iinss2  4367  iinab  4376  iinun2  4381  iundif2  4382  iindif2  4384  iinin2  4385  elriin  4388  iinpw  4404  xpiindi  5128  cnviin  5534  iinpreima  6002  iiner  7385  ixpiin  7497  boxriin  7513  iunocv  18585  hauscmplem  19779  txtube  20014  isfcls  20383  iscmet3  21605  taylfval  22626  fnemeet1  30159  kelac1  30984  diaglbN  36522  dibglbN  36633  dihglbcpreN  36767
  Copyright terms: Public domain W3C validator