Theorem eliin 3975

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 2413	. . 3 |- (y = A -> (y e. C <-> A e. C))
2	1	ralbidv 2635	. 2 |- (y = A -> (A.x e. B y e. C <-> A.x e. B A e. C))
3		df-iin 3973	. 2 |- |^|_x e. B C = {y | A.x e. B y e. C}
4	2, 3	elab2g 2988	1 |- (A e. V -> (A e. |^|_x e. B C <-> A.x e. B A e. C))

Syntax hints:   -> wi 4   <-> wb 176   = wceq 1642   e. wcel 1710  A.wral 2615  |^|_ciin 3971

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ral 2620  df-v 2862  df-iin 3973

This theorem is referenced by:  iinconst  3979  iuniin  3980  iinss1  3982  ssiinf  4016  iinss  4018  iinss2  4019  iinab  4028  iinun2  4033  iundif2  4034  iindif2  4036  iinin2  4037  elriin  4039  iinxprg  4044  iinuni  4050  iinpw  4055  cnviin  5119