Theorem mpt2eq3dva 6387

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 1216	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3	2	eqeq2d 2472	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C <-> z = D ) )
4	3	pm5.32da 651	. . 3 |- ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ z = D ) ) )
5	4	oprabbidv 6377	. 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 6325	. 2 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7		df-mpt2 6325	. 2 |- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8	5, 6, 7	3eqtr4g 2521	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Syntax hints:   -> wi 4   /\ wa 375   /\ w3a 991   = wceq 1455   e. wcel 1898   {coprab 6321   |-> cmpt2 6322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-oprab 6324  df-mpt2 6325

This theorem is referenced by:  mpt2eq3ia  6388  mpt2eq3dv  6389  ofeq  6565  fmpt2co  6911  mapxpen  7769  cantnffval  8199  cantnfres  8213  sadfval  14481  smufval  14506  vdwapfval  14976  comfeq  15666  monpropd  15697  cofuval2  15847  cofuass  15849  cofulid  15850  cofurid  15851  catcisolem  16056  prfval  16139  prf1st  16144  prf2nd  16145  1st2ndprf  16146  xpcpropd  16148  curf1  16165  curfuncf  16178  curf2ndf  16187  grpsubpropd2  16812  mulgpropd  16846  oppglsm  17349  subglsm  17378  lsmpropd  17382  gsumcom2  17662  gsumdixp  17892  psrvscafval  18669  evlslem4  18786  evlslem2  18790  psrplusgpropd  18884  mamures  19470  mpt2matmul  19526  mamutpos  19538  dmatmul  19577  dmatcrng  19582  scmatscmiddistr  19588  scmatcrng  19601  1marepvmarrepid  19655  1marepvsma1  19663  mdetrsca2  19684  mdetrlin2  19687  mdetunilem5  19696  mdetunilem6  19697  mdetunilem7  19698  mdetunilem8  19699  mdetunilem9  19700  maduval  19718  maducoeval  19719  maducoeval2  19720  madugsum  19723  madurid  19724  smadiadetglem2  19752  cramerimplem2  19764  mat2pmatghm  19809  mat2pmatmul  19810  m2cpminvid  19832  m2cpminvid2  19834  decpmatid  19849  decpmatmulsumfsupp  19852  monmatcollpw  19858  pmatcollpwscmatlem2  19869  mp2pm2mplem3  19887  mp2pm2mplem4  19888  pm2mpghm  19895  pm2mpmhmlem1  19897  ptval2  20671  cnmpt2t  20743  cnmpt22  20744  cnmptcom  20748  cnmptk2  20756  cnmpt2plusg  21158  istgp2  21161  prdstmdd  21193  cnmpt2vsca  21264  cnmpt2ds  21916  cnmpt2pc  22011  cnmpt2ip  22274  rrxds  22407  rrxmfval  22415  nvmfval  26321  mdetpmtr12  28702  madjusmdetlem1  28704  pstmval  28749  sseqval  29271  cvmlift2lem6  30081  cvmlift2lem7  30082  cvmlift2lem12  30087  dvhfvadd  34705  funcrngcsetcALT  40370