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

Metamath Proof Explorer

Theorem mpoeq3dva

Description: Slightly more general equality inference for the maps-to notation. (Contributed by NM, 17-Oct-2013)

Ref Expression
Hypothesis mpoeq3dva.1 
|- ( ( ph /\ x e. A /\ y e. B ) -> C = D )
Assertion mpoeq3dva 
|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Proof

Step Hyp Ref Expression
1 mpoeq3dva.1 
 |-  ( ( ph /\ x e. A /\ y e. B ) -> C = D )
2 1 3expb 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3 2 eqeq2d 
 |-  ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C <-> z = D ) )
4 3 pm5.32da 
 |-  ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ z = D ) ) )
5 4 oprabbidv 
 |-  ( ph -> { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) } )
6 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7 df-mpo 
 |-  ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8 5 6 7 3eqtr4g 
 |-  ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )