Metamath Proof Explorer

Theorem mpoeq123dva

Description: An equality deduction for the maps-to notation. (Contributed by Mario Carneiro, 26-Jan-2017)

Ref Expression
Hypotheses mpoeq123dv.1 
|- ( ph -> A = D )
mpoeq123dva.2 
|- ( ( ph /\ x e. A ) -> B = E )
mpoeq123dva.3 
|- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = F )
Assertion mpoeq123dva 
|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )

Proof

Step Hyp Ref Expression
1 mpoeq123dv.1 
 |-  ( ph -> A = D )
2 mpoeq123dva.2 
 |-  ( ( ph /\ x e. A ) -> B = E )
3 mpoeq123dva.3 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = F )
4 3 eqeq2d 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C <-> z = F ) )
5 4 pm5.32da 
 |-  ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ z = F ) ) )
6 2 eleq2d 
 |-  ( ( ph /\ x e. A ) -> ( y e. B <-> y e. E ) )
7 6 pm5.32da 
 |-  ( ph -> ( ( x e. A /\ y e. B ) <-> ( x e. A /\ y e. E ) ) )
8 1 eleq2d 
 |-  ( ph -> ( x e. A <-> x e. D ) )
9 8 anbi1d 
 |-  ( ph -> ( ( x e. A /\ y e. E ) <-> ( x e. D /\ y e. E ) ) )
10 7 9 bitrd 
 |-  ( ph -> ( ( x e. A /\ y e. B ) <-> ( x e. D /\ y e. E ) ) )
11 10 anbi1d 
 |-  ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = F ) <-> ( ( x e. D /\ y e. E ) /\ z = F ) ) )
12 5 11 bitrd 
 |-  ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. D /\ y e. E ) /\ z = F ) ) )
13 12 oprabbidv 
 |-  ( ph -> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { <. <. x , y >. , z >. | ( ( x e. D /\ y e. E ) /\ z = F ) } )
14 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
15 df-mpo 
 |-  ( x e. D , y e. E |-> F ) = { <. <. x , y >. , z >. | ( ( x e. D /\ y e. E ) /\ z = F ) }
16 13 14 15 3eqtr4g 
 |-  ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )