Theorem iunssdf

Description: Subset theorem for an indexed union. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	iunssdf.1	|- F/ x ph
	iunssdf.2	|- F/_ x C
	iunssdf.3	|- ( ( ph /\ x e. A ) -> B C_ C )
Assertion	iunssdf	|- ( ph -> U_ x e. A B C_ C )

Proof

Step	Hyp	Ref	Expression
1		iunssdf.1	|- F/ x ph
2		iunssdf.2	|- F/_ x C
3		iunssdf.3	|- ( ( ph /\ x e. A ) -> B C_ C )
4	1 3	ralrimia	|- ( ph -> A. x e. A B C_ C )
5	2	iunssf	|- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )
6	4 5	sylibr	|- ( ph -> U_ x e. A B C_ C )