Theorem eliin 4321

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 2515	. . 3 |- ( y = A -> ( y e. C <-> A e. C ) )
2	1	ralbidv 2882	. 2 |- ( y = A -> ( A. x e. B y e. C <-> A. x e. B A e. C ) )
3		df-iin 4318	. 2 |- |^|_ x e. B C = { y | A. x e. B y e. C }
4	2, 3	elab2g 3234	1 |- ( A e. V -> ( A e. |^|_ x e. B C <-> A. x e. B A e. C ) )

Syntax hints:   -> wi 4   <-> wb 184   = wceq 1383   e. wcel 1804   A.wral 2793   |^|_ciin 4316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ral 2798  df-v 3097  df-iin 4318

This theorem is referenced by:  iinconst  4325  iuniin  4326  iinss1  4328  ssiinf  4364  iinss  4366  iinss2  4367  iinab  4376  iinun2  4381  iundif2  4382  iindif2  4384  iinin2  4385  elriin  4388  iinpw  4404  xpiindi  5128  cnviin  5534  iinpreima  6002  iiner  7385  ixpiin  7497  boxriin  7513  iunocv  18585  hauscmplem  19779  txtube  20014  isfcls  20383  iscmet3  21605  taylfval  22626  fnemeet1  30159  kelac1  30984  diaglbN  36522  dibglbN  36633  dihglbcpreN  36767