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

Metamath Proof Explorer

Theorem iuncom

Description: Commutation of indexed unions. (Contributed by NM, 18-Dec-2008)

Ref Expression
Assertion iuncom 
|- U_ x e. A U_ y e. B C = U_ y e. B U_ x e. A C

Proof

Step Hyp Ref Expression
1 rexcom 
 |-  ( E. x e. A E. y e. B z e. C <-> E. y e. B E. x e. A z e. C )
2 eliun 
 |-  ( z e. U_ y e. B C <-> E. y e. B z e. C )
3 2 rexbii 
 |-  ( E. x e. A z e. U_ y e. B C <-> E. x e. A E. y e. B z e. C )
4 eliun 
 |-  ( z e. U_ x e. A C <-> E. x e. A z e. C )
5 4 rexbii 
 |-  ( E. y e. B z e. U_ x e. A C <-> E. y e. B E. x e. A z e. C )
6 1 3 5 3bitr4i 
 |-  ( E. x e. A z e. U_ y e. B C <-> E. y e. B z e. U_ x e. A C )
7 eliun 
 |-  ( z e. U_ x e. A U_ y e. B C <-> E. x e. A z e. U_ y e. B C )
8 eliun 
 |-  ( z e. U_ y e. B U_ x e. A C <-> E. y e. B z e. U_ x e. A C )
9 6 7 8 3bitr4i 
 |-  ( z e. U_ x e. A U_ y e. B C <-> z e. U_ y e. B U_ x e. A C )
10 9 eqriv 
 |-  U_ x e. A U_ y e. B C = U_ y e. B U_ x e. A C