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

Metamath Proof Explorer

Theorem iuneq12daf

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017)

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

Proof

Step Hyp Ref Expression
1 iuneq12daf.1 
 |-  F/ x ph
2 iuneq12daf.2 
 |-  F/_ x A
3 iuneq12daf.3 
 |-  F/_ x B
4 iuneq12daf.4 
 |-  ( ph -> A = B )
5 iuneq12daf.5 
 |-  ( ( ph /\ x e. A ) -> C = D )
6 5 eleq2d 
 |-  ( ( ph /\ x e. A ) -> ( y e. C <-> y e. D ) )
7 1 6 rexbida 
 |-  ( ph -> ( E. x e. A y e. C <-> E. x e. A y e. D ) )
8 2 3 rexeqf 
 |-  ( A = B -> ( E. x e. A y e. D <-> E. x e. B y e. D ) )
9 4 8 syl 
 |-  ( ph -> ( E. x e. A y e. D <-> E. x e. B y e. D ) )
10 7 9 bitrd 
 |-  ( ph -> ( E. x e. A y e. C <-> E. x e. B y e. D ) )
11 10 alrimiv 
 |-  ( ph -> A. y ( E. x e. A y e. C <-> E. x e. B y e. D ) )
12 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 } )
13 df-iun 
 |-  U_ x e. A C = { y | E. x e. A y e. C }
14 df-iun 
 |-  U_ x e. B D = { y | E. x e. B y e. D }
15 12 13 14 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 )
16 11 15 syl 
 |-  ( ph -> U_ x e. A C = U_ x e. B D )