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

Metamath Proof Explorer

Theorem iunxpf

Description: Indexed union on a Cartesian product equals a double indexed union. The hypothesis specifies an implicit substitution. (Contributed by NM, 19-Dec-2008)

Ref Expression
Hypotheses iunxpf.1 
|- F/_ y C
iunxpf.2 
|- F/_ z C
iunxpf.3 
|- F/_ x D
iunxpf.4 
|- ( x = <. y , z >. -> C = D )
Assertion iunxpf 
|- U_ x e. ( A X. B ) C = U_ y e. A U_ z e. B D

Proof

Step Hyp Ref Expression
1 iunxpf.1 
 |-  F/_ y C
2 iunxpf.2 
 |-  F/_ z C
3 iunxpf.3 
 |-  F/_ x D
4 iunxpf.4 
 |-  ( x = <. y , z >. -> C = D )
5 1 nfcri 
 |-  F/ y w e. C
6 2 nfcri 
 |-  F/ z w e. C
7 3 nfcri 
 |-  F/ x w e. D
8 4 eleq2d 
 |-  ( x = <. y , z >. -> ( w e. C <-> w e. D ) )
9 5 6 7 8 rexxpf 
 |-  ( E. x e. ( A X. B ) w e. C <-> E. y e. A E. z e. B w e. D )
10 eliun 
 |-  ( w e. U_ x e. ( A X. B ) C <-> E. x e. ( A X. B ) w e. C )
11 eliun 
 |-  ( w e. U_ y e. A U_ z e. B D <-> E. y e. A w e. U_ z e. B D )
12 eliun 
 |-  ( w e. U_ z e. B D <-> E. z e. B w e. D )
13 12 rexbii 
 |-  ( E. y e. A w e. U_ z e. B D <-> E. y e. A E. z e. B w e. D )
14 11 13 bitri 
 |-  ( w e. U_ y e. A U_ z e. B D <-> E. y e. A E. z e. B w e. D )
15 9 10 14 3bitr4i 
 |-  ( w e. U_ x e. ( A X. B ) C <-> w e. U_ y e. A U_ z e. B D )
16 15 eqriv 
 |-  U_ x e. ( A X. B ) C = U_ y e. A U_ z e. B D