Theorem mpt2eq3dva 6345

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 1197	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3	2	eqeq2d 2481	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C <-> z = D ) )
4	3	pm5.32da 641	. . 3 |- ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ z = D ) ) )
5	4	oprabbidv 6335	. 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 6289	. 2 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7		df-mpt2 6289	. 2 |- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8	5, 6, 7	3eqtr4g 2533	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 973   = wceq 1379   e. wcel 1767   {coprab 6285   |-> cmpt2 6286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-oprab 6288  df-mpt2 6289

This theorem is referenced by:  mpt2eq3ia  6346  mpt2eq3dv  6347  ofeq  6526  fmpt2co  6866  seqomeq12  7119  mapxpen  7683  cantnffval  8080  cantnfres  8096  cantnfvalOLD  8117  sadfval  13961  smufval  13986  vdwapfval  14348  comfeq  14962  monpropd  14993  cofuval2  15114  cofuass  15116  cofulid  15117  cofurid  15118  catcisolem  15291  prfval  15326  prf1st  15331  prf2nd  15332  1st2ndprf  15333  xpcpropd  15335  curf1  15352  curfuncf  15365  curf2ndf  15374  grpsubpropd2  15951  mulgpropd  15985  lsmfval  16464  oppglsm  16468  subglsm  16497  lsmpropd  16501  gsumcom2  16806  gsumdixpOLD  17058  gsumdixp  17059  psrvscafval  17842  evlslem4OLD  17972  evlslem4  17973  evlslem2  17979  psrplusgpropd  18076  mamures  18687  mpt2matmul  18743  mamutpos  18755  dmatmul  18794  dmatcrng  18799  scmatscmiddistr  18805  scmatcrng  18818  1marepvmarrepid  18872  1marepvsma1  18880  mdetrsca2  18901  mdetrlin2  18904  mdetunilem5  18913  mdetunilem6  18914  mdetunilem7  18915  mdetunilem8  18916  mdetunilem9  18917  madufval  18934  maduval  18935  maducoeval  18936  maducoeval2  18937  madugsum  18940  madurid  18941  smadiadetglem2  18969  cramerimplem2  18981  mat2pmatghm  19026  mat2pmatmul  19027  m2cpminvid  19049  m2cpminvid2  19051  decpmatid  19066  decpmatmulsumfsupp  19069  monmatcollpw  19075  pmatcollpwscmatlem2  19086  mp2pm2mplem3  19104  mp2pm2mplem4  19105  pm2mpghm  19112  pm2mpmhmlem1  19114  ptval2  19865  cnmpt2t  19937  cnmpt22  19938  cnmptcom  19942  cnmptk2  19950  cnmpt2plusg  20350  istgp2  20353  prdstmdd  20385  cnmpt2vsca  20460  cnmpt2ds  21111  cnmpt2pc  21191  cnmpt2ip  21451  rrxds  21588  rrxmfval  21596  ttgval  23882  nvmfval  25243  pstmval  27538  ofceq  27764  sseqval  27995  cvmlift2lem6  28421  cvmlift2lem7  28422  cvmlift2lem12  28427  dvhfvadd  35906