Metamath Proof Explorer


Theorem iunss

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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-iun
 |-  U_ x e. A B = { y | E. x e. A y e. B }
2 1 sseq1i
 |-  ( U_ x e. A B C_ C <-> { y | E. x e. A y e. B } C_ C )
3 abss
 |-  ( { y | E. x e. A y e. B } C_ C <-> A. y ( E. x e. A y e. B -> y e. C ) )
4 dfss2
 |-  ( B C_ C <-> A. y ( y e. B -> y e. C ) )
5 4 ralbii
 |-  ( A. x e. A B C_ C <-> A. x e. A A. y ( y e. B -> y e. C ) )
6 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 ) )
7 r19.23v
 |-  ( A. x e. A ( y e. B -> y e. C ) <-> ( E. x e. A y e. B -> y e. C ) )
8 7 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 ) )
9 5 6 8 3bitrri
 |-  ( A. y ( E. x e. A y e. B -> y e. C ) <-> A. x e. A B C_ C )
10 2 3 9 3bitri
 |-  ( U_ x e. A B C_ C <-> A. x e. A B C_ C )