Theorem mpt2eq3dva 6342

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 1198	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3	2	eqeq2d 2416	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C <-> z = D ) )
4	3	pm5.32da 639	. . 3 |- ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ z = D ) ) )
5	4	oprabbidv 6332	. 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 6283	. 2 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7		df-mpt2 6283	. 2 |- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8	5, 6, 7	3eqtr4g 2468	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Syntax hints:   -> wi 4   /\ wa 367   /\ w3a 974   = wceq 1405   e. wcel 1842   {coprab 6279   |-> cmpt2 6280

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380

This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-oprab 6282  df-mpt2 6283

This theorem is referenced by:  mpt2eq3ia  6343  mpt2eq3dv  6344  ofeq  6523  fmpt2co  6867  mapxpen  7721  cantnffval  8112  cantnfres  8128  cantnfvalOLD  8149  sadfval  14311  smufval  14336  vdwapfval  14698  comfeq  15319  monpropd  15350  cofuval2  15500  cofuass  15502  cofulid  15503  cofurid  15504  catcisolem  15709  prfval  15792  prf1st  15797  prf2nd  15798  1st2ndprf  15799  xpcpropd  15801  curf1  15818  curfuncf  15831  curf2ndf  15840  grpsubpropd2  16465  mulgpropd  16499  oppglsm  16986  subglsm  17015  lsmpropd  17019  gsumcom2  17324  gsumdixpOLD  17577  gsumdixp  17578  psrvscafval  18363  evlslem4OLD  18493  evlslem4  18494  evlslem2  18500  psrplusgpropd  18597  mamures  19184  mpt2matmul  19240  mamutpos  19252  dmatmul  19291  dmatcrng  19296  scmatscmiddistr  19302  scmatcrng  19315  1marepvmarrepid  19369  1marepvsma1  19377  mdetrsca2  19398  mdetrlin2  19401  mdetunilem5  19410  mdetunilem6  19411  mdetunilem7  19412  mdetunilem8  19413  mdetunilem9  19414  maduval  19432  maducoeval  19433  maducoeval2  19434  madugsum  19437  madurid  19438  smadiadetglem2  19466  cramerimplem2  19478  mat2pmatghm  19523  mat2pmatmul  19524  m2cpminvid  19546  m2cpminvid2  19548  decpmatid  19563  decpmatmulsumfsupp  19566  monmatcollpw  19572  pmatcollpwscmatlem2  19583  mp2pm2mplem3  19601  mp2pm2mplem4  19602  pm2mpghm  19609  pm2mpmhmlem1  19611  ptval2  20394  cnmpt2t  20466  cnmpt22  20467  cnmptcom  20471  cnmptk2  20479  cnmpt2plusg  20879  istgp2  20882  prdstmdd  20914  cnmpt2vsca  20989  cnmpt2ds  21640  cnmpt2pc  21720  cnmpt2ip  21980  rrxds  22117  rrxmfval  22125  nvmfval  25953  pstmval  28327  sseqval  28833  cvmlift2lem6  29605  cvmlift2lem7  29606  cvmlift2lem12  29611  dvhfvadd  34111  funcrngcsetcALT  38318