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

Theorem eliin 4303
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 2865 . 2  |-  ( y  =  A  ->  ( A. x  e.  B  y  e.  C  <->  A. x  e.  B  A  e.  C ) )
3 df-iin 4300 . 2  |-  |^|_ x  e.  B  C  =  { y  |  A. x  e.  B  y  e.  C }
42, 3elab2g 3221 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 1438    e. wcel 1869   A.wral 2776   |^|_ciin 4298
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ral 2781  df-v 3084  df-iin 4300
This theorem is referenced by:  iinconst  4307  iuniin  4308  iinss1  4310  ssiinf  4346  iinss  4348  iinss2  4349  iinab  4358  iinun2  4363  iundif2  4364  iindif2  4366  iinin2  4367  elriin  4370  iinpw  4389  xpiindi  4987  cnviin  5390  iinpreima  6023  iiner  7441  ixpiin  7554  boxriin  7570  iunocv  19236  hauscmplem  20413  txtube  20647  isfcls  21016  iscmet3  22255  taylfval  23306  fnemeet1  31021  diaglbN  34586  dibglbN  34697  dihglbcpreN  34831  kelac1  35885
  Copyright terms: Public domain W3C validator