Theorem iunssd

Description: Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypothesis	iunssd.1	|- ( ( ph /\ x e. A ) -> B C_ C )
Assertion	iunssd	|- ( ph -> U_ x e. A B C_ C )

Proof

Step	Hyp	Ref	Expression
1		iunssd.1	|- ( ( ph /\ x e. A ) -> B C_ C )
2	1	ralrimiva	|- ( ph -> A. x e. A B C_ C )
3		iunss	|- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )
4	2 3	sylibr	|- ( ph -> U_ x e. A B C_ C )