Theorem mpt2eq3dva 6258

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 1189	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3	2	eqeq2d 2468	. . . 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 6248	. 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 6204	. 2 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7		df-mpt2 6204	. 2 |- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8	5, 6, 7	3eqtr4g 2520	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   = wceq 1370   e. wcel 1758   {coprab 6200   |-> cmpt2 6201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-oprab 6203  df-mpt2 6204

This theorem is referenced by:  mpt2eq3ia  6259  mpt2eq3dv  6260  ofeq  6431  fmpt2co  6765  seqomeq12  7018  mapxpen  7586  cantnffval  7979  cantnfres  7995  cantnfvalOLD  8016  sadfval  13765  smufval  13790  vdwapfval  14149  comfeq  14763  monpropd  14794  cofuval2  14915  cofuass  14917  cofulid  14918  cofurid  14919  catcisolem  15092  prfval  15127  prf1st  15132  prf2nd  15133  1st2ndprf  15134  xpcpropd  15136  curf1  15153  curfuncf  15166  curf2ndf  15175  grpsubpropd2  15745  mulgpropd  15778  lsmfval  16257  oppglsm  16261  subglsm  16290  lsmpropd  16294  gsumcom2  16588  gsumdixpOLD  16822  gsumdixp  16823  psrvscafval  17583  evlslem4OLD  17713  evlslem4  17714  evlslem2  17720  psrplusgpropd  17813  mamures  18414  mamutpos  18469  1marepvmarrepid  18512  1marepvsma1  18520  mdetrsca2  18541  mdetrlin2  18544  mdetunilem5  18553  mdetunilem6  18554  mdetunilem7  18555  mdetunilem8  18556  mdetunilem9  18557  madufval  18574  maduval  18575  maducoeval  18576  maducoeval2  18577  madugsum  18580  madurid  18581  smadiadetglem2  18609  cramerimplem2  18621  ptval2  19305  cnmpt2t  19377  cnmpt22  19378  cnmptcom  19382  cnmptk2  19390  cnmpt2plusg  19790  istgp2  19793  prdstmdd  19825  cnmpt2vsca  19900  cnmpt2ds  20551  cnmpt2pc  20631  cnmpt2ip  20891  rrxds  21028  rrxmfval  21036  ttgval  23272  nvmfval  24175  pstmval  26466  ofceq  26683  sseqval  26914  cvmlift2lem6  27340  cvmlift2lem7  27341  cvmlift2lem12  27346  mpt2matmul  31027  dmatmul  31041  dmatcrng  31046  scmatcrng  31053  mat2pmatghm  31205  mat2pmatmul  31206  m2pminv  31223  m2pminv2  31225  decpmatid  31243  decpmatmulsumfsupp  31246  monmatcollpw  31252  pmatcollpwscmatlem2  31262  mp2pm2mplem3  31280  mp2pm2mplem4  31281  pm2mpghm  31288  pm2mpmhmlem1  31290  cpmadumatpolylem2  31353  dvhfvadd  35059