Theorem ssiun3

Description: Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016)

	Ref	Expression
Assertion	ssiun3	|- ( A. y e. C E. x e. A y e. B <-> C C_ U_ x e. A B )

Proof

Step	Hyp	Ref	Expression
1		dfss2	|- ( C C_ U_ x e. A B <-> A. y ( y e. C -> y e. U_ x e. A B ) )
2		df-ral	|- ( A. y e. C y e. U_ x e. A B <-> A. y ( y e. C -> y e. U_ x e. A B ) )
3		eliun	|- ( y e. U_ x e. A B <-> E. x e. A y e. B )
4	3	ralbii	|- ( A. y e. C y e. U_ x e. A B <-> A. y e. C E. x e. A y e. B )
5	1 2 4	3bitr2ri	|- ( A. y e. C E. x e. A y e. B <-> C C_ U_ x e. A B )