Theorem iunss

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011) Avoid ax-10 , ax-12 . (Revised by SN, 2-Feb-2026)

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

Proof

Step	Hyp	Ref	Expression
1		df-ss	|- ( U_ x e. A B C_ C <-> A. y ( y e. U_ x e. A B -> y e. C ) )
2		eliun	|- ( y e. U_ x e. A B <-> E. x e. A y e. B )
3	2	imbi1i	|- ( ( y e. U_ x e. A B -> y e. C ) <-> ( E. x e. A y e. B -> y e. C ) )
4	3	albii	|- ( A. y ( y e. U_ x e. A B -> y e. C ) <-> A. y ( E. x e. A y e. B -> y e. C ) )
5		df-ss	|- ( B C_ C <-> A. y ( y e. B -> y e. C ) )
6	5	ralbii	|- ( A. x e. A B C_ C <-> A. x e. A A. y ( y e. B -> y e. C ) )
7		ralcom4	|- ( A. x e. A A. y ( y e. B -> y e. C ) <-> A. y A. x e. A ( y e. B -> y e. C ) )
8		r19.23v	|- ( A. x e. A ( y e. B -> y e. C ) <-> ( E. x e. A y e. B -> y e. C ) )
9	8	albii	|- ( A. y A. x e. A ( y e. B -> y e. C ) <-> A. y ( E. x e. A y e. B -> y e. C ) )
10	6 7 9	3bitrri	|- ( A. y ( E. x e. A y e. B -> y e. C ) <-> A. x e. A B C_ C )
11	1 4 10	3bitri	|- ( U_ x e. A B C_ C <-> A. x e. A B C_ C )