Theorem uniin2

Description: Union of intersection. Generalization of half of theorem "Distributive laws" in Enderton p. 30. (Contributed by Thierry Arnoux, 21-Jun-2020)

	Ref	Expression
Assertion	uniin2	|- U_ x e. B ( A i^i x ) = ( A i^i U. B )

Proof

Step	Hyp	Ref	Expression
1		iunin2	|- U_ x e. B ( A i^i x ) = ( A i^i U_ x e. B x )
2		uniiun	|- U. B = U_ x e. B x
3	2	ineq2i	|- ( A i^i U. B ) = ( A i^i U_ x e. B x )
4	1 3	eqtr4i	|- U_ x e. B ( A i^i x ) = ( A i^i U. B )