Metamath Proof Explorer


Theorem iniin1

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

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

Proof

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