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.

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

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