Theorem iinin2

Description: Indexed intersection of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. Use intiin to recover Enderton's theorem. (Contributed by Mario Carneiro, 19-Mar-2015)

	Ref	Expression
Assertion	iinin2	|- ( A =/= (/) -> |^|_ x e. A ( B i^i C ) = ( B i^i |^|_ x e. A C ) )

Proof

Step	Hyp	Ref	Expression
1		r19.28zv	|- ( A =/= (/) -> ( A. x e. A ( y e. B /\ y e. C ) <-> ( y e. B /\ A. x e. A y e. C ) ) )
2		elin	|- ( y e. ( B i^i C ) <-> ( y e. B /\ y e. C ) )
3	2	ralbii	|- ( A. x e. A y e. ( B i^i C ) <-> A. x e. A ( y e. B /\ y e. C ) )
4		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A C <-> A. x e. A y e. C ) )
5	4	elv	|- ( y e. |^|_ x e. A C <-> A. x e. A y e. C )
6	5	anbi2i	|- ( ( y e. B /\ y e. |^|_ x e. A C ) <-> ( y e. B /\ A. x e. A y e. C ) )
7	1 3 6	3bitr4g	|- ( A =/= (/) -> ( A. x e. A y e. ( B i^i C ) <-> ( y e. B /\ y e. |^|_ x e. A C ) ) )
8		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A ( B i^i C ) <-> A. x e. A y e. ( B i^i C ) ) )
9	8	elv	|- ( y e. |^|_ x e. A ( B i^i C ) <-> A. x e. A y e. ( B i^i C ) )
10		elin	|- ( y e. ( B i^i |^|_ x e. A C ) <-> ( y e. B /\ y e. |^|_ x e. A C ) )
11	7 9 10	3bitr4g	|- ( A =/= (/) -> ( y e. |^|_ x e. A ( B i^i C ) <-> y e. ( B i^i |^|_ x e. A C ) ) )
12	11	eqrdv	|- ( A =/= (/) -> |^|_ x e. A ( B i^i C ) = ( B i^i |^|_ x e. A C ) )