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.

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

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