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

Metamath Proof Explorer

Theorem iuneq12df

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016)

Ref Expression
Hypotheses iuneq12df.1 
|- F/ x ph
iuneq12df.2 
|- F/_ x A
iuneq12df.3 
|- F/_ x B
iuneq12df.4 
|- ( ph -> A = B )
iuneq12df.5 
|- ( ph -> C = D )
Assertion iuneq12df 
|- ( ph -> U_ x e. A C = U_ x e. B D )

Proof

Step Hyp Ref Expression
1 iuneq12df.1 
 |-  F/ x ph
2 iuneq12df.2 
 |-  F/_ x A
3 iuneq12df.3 
 |-  F/_ x B
4 iuneq12df.4 
 |-  ( ph -> A = B )
5 iuneq12df.5 
 |-  ( ph -> C = D )
6 5 eleq2d 
 |-  ( ph -> ( y e. C <-> y e. D ) )
7 1 2 3 4 6 rexeqbid 
 |-  ( ph -> ( E. x e. A y e. C <-> E. x e. B y e. D ) )
8 7 alrimiv 
 |-  ( ph -> A. y ( E. x e. A y e. C <-> E. x e. B y e. D ) )
9 abbi 
 |-  ( A. y ( E. x e. A y e. C <-> E. x e. B y e. D ) -> { y | E. x e. A y e. C } = { y | E. x e. B y e. D } )
10 df-iun 
 |-  U_ x e. A C = { y | E. x e. A y e. C }
11 df-iun 
 |-  U_ x e. B D = { y | E. x e. B y e. D }
12 9 10 11 3eqtr4g 
 |-  ( A. y ( E. x e. A y e. C <-> E. x e. B y e. D ) -> U_ x e. A C = U_ x e. B D )
13 8 12 syl 
 |-  ( ph -> U_ x e. A C = U_ x e. B D )