This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )