Theorem mpt2eq3dva 6097

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

Hypothesis

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

Assertion

Ref	Expression
mpt2eq3dva	|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   A( x, y)   B( x, y)   C( x, y)   D( x, y)

Proof of Theorem mpt2eq3dva

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpt2eq3dva.1	. . . . . 6 |- ( ( ph /\ x e. A /\ y e. B ) -> C = D )
2	1	3expb 1154	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3	2	eqeq2d 2415	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C <-> z = D ) )
4	3	pm5.32da 623	. . 3 |- ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ z = D ) ) )
5	4	oprabbidv 6087	. 2 |- ( 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-mpt2 6045	. 2 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7		df-mpt2 6045	. 2 |- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8	5, 6, 7	3eqtr4g 2461	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Syntax hints:   -> wi 4   /\ wa 359   /\ w3a 936   = wceq 1649   e. wcel 1721   {coprab 6041   e. cmpt2 6042

This theorem is referenced by:  mpt2eq3ia  6098  ofeq  6266  fmpt2co  6389  seqomeq12  6670  mapxpen  7232  cantnffval  7574  cantnfval  7579  cantnfres  7589  sadfval  12919  smufval  12944  vdwapfval  13294  comfeq  13887  monpropd  13918  cofuval2  14039  cofuass  14041  cofulid  14042  cofurid  14043  catcisolem  14216  prfval  14251  prf1st  14256  prf2nd  14257  1st2ndprf  14258  xpcpropd  14260  curf1  14277  curfuncf  14290  curf2ndf  14299  odumeet  14522  odujoin  14524  grpsubpropd2  14845  mulgpropd  14878  lsmfval  15227  oppglsm  15231  subglsm  15260  lsmpropd  15264  gsumcom2  15504  gsumdixp  15670  psrvscafval  16409  evlslem4  16519  evlslem2  16523  psrplusgpropd  16584  ptval2  17586  cnmpt2t  17658  cnmpt22  17659  cnmptcom  17663  cnmptk2  17671  cnmpt2plusg  18071  istgp2  18074  prdstmdd  18106  cnmpt2vsca  18177  cnmpt2ds  18827  cnmpt2pc  18906  cnmpt2ip  19155  nvmfval  22078  pstmval  24243  ofceq  24433  cvmlift2lem6  24948  cvmlift2lem7  24949  cvmlift2lem12  24954  dvhfvadd  31574

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-oprab 6044  df-mpt2 6045