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

Theorem eliin 4276
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 2474 . . 3  |-  ( y  =  A  ->  (
y  e.  C  <->  A  e.  C ) )
21ralbidv 2842 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  C  <->  A. x  e.  B  A  e.  C ) )
3 df-iin 4273 . 2  |-  |^|_ x  e.  B  C  =  { y  |  A. x  e.  B  y  e.  C }
42, 3elab2g 3197 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 1405    e. wcel 1842   A.wral 2753   |^|_ciin 4271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2758  df-v 3060  df-iin 4273
This theorem is referenced by:  iinconst  4280  iuniin  4281  iinss1  4283  ssiinf  4319  iinss  4321  iinss2  4322  iinab  4331  iinun2  4336  iundif2  4337  iindif2  4339  iinin2  4340  elriin  4343  iinpw  4362  xpiindi  4958  cnviin  5360  iinpreima  5994  iiner  7419  ixpiin  7532  boxriin  7548  iunocv  19008  hauscmplem  20197  txtube  20431  isfcls  20800  iscmet3  22022  taylfval  23044  fnemeet1  30581  diaglbN  34055  dibglbN  34166  dihglbcpreN  34300  kelac1  35351
  Copyright terms: Public domain W3C validator