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

Metamath Proof Explorer

Theorem iniin2

Description: Indexed intersection of intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 iinin2 
 |-  ( A =/= (/) -> |^|_ x e. A ( B i^i C ) = ( B i^i |^|_ x e. A C ) )
2 1 eqcomd 
 |-  ( A =/= (/) -> ( B i^i |^|_ x e. A C ) = |^|_ x e. A ( B i^i C ) )