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