Theorem eliin 3826

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

Syntax hints:   -> wi 4   <-> wb 104   = wceq 1332   e. wcel 1481   A.wral 2417   |^|_ciin 3822

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691  df-iin 3824

This theorem is referenced by:  iinconstm  3830  iuniin  3831  iinss1  3833  ssiinf  3870  iinss  3872  iinss2  3873  iinab  3882  iundif2ss  3886  iindif2m  3888  iinin2m  3889  elriin  3891  iinpw  3911  xpiindim  4684  cnviinm  5088  iinerm  6509  ixpiinm  6626