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 ) )