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

Theorem eliin 4287
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 2519 . . 3  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
21ralbidv 2829 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  C  <->  A. x  e.  B  A  e.  C ) )
3 df-iin 4284 . 2  |-  |^|_ x  e.  B  C  =  { y  |  A. x  e.  B  y  e.  C }
42, 3elab2g 3189 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 188    = wceq 1446    e. wcel 1889   A.wral 2739   |^|_ciin 4282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ral 2744  df-v 3049  df-iin 4284
This theorem is referenced by:  iinconst  4291  iuniin  4292  iinss1  4294  ssiinf  4330  iinss  4332  iinss2  4333  iinab  4342  iinun2  4347  iundif2  4348  iindif2  4350  iinin2  4351  elriin  4354  iinpw  4373  xpiindi  4973  cnviin  5376  iinpreima  6015  iiner  7440  ixpiin  7553  boxriin  7569  iunocv  19256  hauscmplem  20433  txtube  20667  isfcls  21036  iscmet3  22275  taylfval  23326  fnemeet1  31034  diaglbN  34635  dibglbN  34746  dihglbcpreN  34880  kelac1  35933  eliind  37425  hspdifhsp  38448
  Copyright terms: Public domain W3C validator