Theorem iinssiun

Description: An indexed intersection is a subset of the corresponding indexed union. (Contributed by Thierry Arnoux, 31-Dec-2021)

	Ref	Expression
Assertion	iinssiun	|- ( A =/= (/) -> |^|_ x e. A B C_ U_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		r19.2z	|- ( ( A =/= (/) /\ A. x e. A y e. B ) -> E. x e. A y e. B )
2	1	ex	|- ( A =/= (/) -> ( A. x e. A y e. B -> E. x e. A y e. B ) )
3		eliin	|- ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
4	3	elv	|- ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
5		eliun	|- ( y e. U_ x e. A B <-> E. x e. A y e. B )
6	2 4 5	3imtr4g	|- ( A =/= (/) -> ( y e. |^|_ x e. A B -> y e. U_ x e. A B ) )
7	6	ssrdv	|- ( A =/= (/) -> |^|_ x e. A B C_ U_ x e. A B )