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

Metamath Proof Explorer

Theorem iuncom4

Description: Commutation of union with indexed union. (Contributed by Mario Carneiro, 18-Jan-2014)

Ref Expression
Assertion iuncom4 
|- U_ x e. A U. B = U. U_ x e. A B

Proof

Step Hyp Ref Expression
1 df-rex 
 |-  ( E. z e. B y e. z <-> E. z ( z e. B /\ y e. z ) )
2 1 rexbii 
 |-  ( E. x e. A E. z e. B y e. z <-> E. x e. A E. z ( z e. B /\ y e. z ) )
3 rexcom4 
 |-  ( E. x e. A E. z ( z e. B /\ y e. z ) <-> E. z E. x e. A ( z e. B /\ y e. z ) )
4 2 3 bitri 
 |-  ( E. x e. A E. z e. B y e. z <-> E. z E. x e. A ( z e. B /\ y e. z ) )
5 r19.41v 
 |-  ( E. x e. A ( z e. B /\ y e. z ) <-> ( E. x e. A z e. B /\ y e. z ) )
6 5 exbii 
 |-  ( E. z E. x e. A ( z e. B /\ y e. z ) <-> E. z ( E. x e. A z e. B /\ y e. z ) )
7 4 6 bitri 
 |-  ( E. x e. A E. z e. B y e. z <-> E. z ( E. x e. A z e. B /\ y e. z ) )
8 eluni2 
 |-  ( y e. U. B <-> E. z e. B y e. z )
9 8 rexbii 
 |-  ( E. x e. A y e. U. B <-> E. x e. A E. z e. B y e. z )
10 df-rex 
 |-  ( E. z e. U_ x e. A B y e. z <-> E. z ( z e. U_ x e. A B /\ y e. z ) )
11 eliun 
 |-  ( z e. U_ x e. A B <-> E. x e. A z e. B )
12 11 anbi1i 
 |-  ( ( z e. U_ x e. A B /\ y e. z ) <-> ( E. x e. A z e. B /\ y e. z ) )
13 12 exbii 
 |-  ( E. z ( z e. U_ x e. A B /\ y e. z ) <-> E. z ( E. x e. A z e. B /\ y e. z ) )
14 10 13 bitri 
 |-  ( E. z e. U_ x e. A B y e. z <-> E. z ( E. x e. A z e. B /\ y e. z ) )
15 7 9 14 3bitr4i 
 |-  ( E. x e. A y e. U. B <-> E. z e. U_ x e. A B y e. z )
16 eliun 
 |-  ( y e. U_ x e. A U. B <-> E. x e. A y e. U. B )
17 eluni2 
 |-  ( y e. U. U_ x e. A B <-> E. z e. U_ x e. A B y e. z )
18 15 16 17 3bitr4i 
 |-  ( y e. U_ x e. A U. B <-> y e. U. U_ x e. A B )
19 18 eqriv 
 |-  U_ x e. A U. B = U. U_ x e. A B