This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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) 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 )