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.

Step	Hyp	Ref	Expression
1		eleq1 2519	. . 3 |- ( y = A -> ( y e. C <-> A e. C ) )
2	1	ralbidv 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 }
4	2, 3	elab2g 3189	1 |- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )

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