Theorem mpt2eq3dva 6719

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 1266	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3	2	eqeq2d 2632	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C <-> z = D ) )
4	3	pm5.32da 673	. . 3 |- ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ z = D ) ) )
5	4	oprabbidv 6709	. 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 6655	. 2 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7		df-mpt2 6655	. 2 |- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8	5, 6, 7	3eqtr4g 2681	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   {coprab 6651   |-> cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  mpt2eq3ia  6720  mpt2eq3dv  6721  ofeq  6899  fmpt2co  7260  mapxpen  8126  cantnffval  8560  cantnfres  8574  sadfval  15174  smufval  15199  vdwapfval  15675  comfeq  16366  monpropd  16397  cofuval2  16547  cofuass  16549  cofulid  16550  cofurid  16551  catcisolem  16756  prfval  16839  prf1st  16844  prf2nd  16845  1st2ndprf  16846  xpcpropd  16848  curf1  16865  curfuncf  16878  curf2ndf  16887  grpsubpropd2  17521  mulgpropd  17584  oppglsm  18057  subglsm  18086  lsmpropd  18090  gsumcom2  18374  gsumdixp  18609  psrvscafval  19390  evlslem4  19508  evlslem2  19512  psrplusgpropd  19606  mamures  20196  mpt2matmul  20252  mamutpos  20264  dmatmul  20303  dmatcrng  20308  scmatscmiddistr  20314  scmatcrng  20327  1marepvmarrepid  20381  1marepvsma1  20389  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  mdetunilem6  20423  mdetunilem7  20424  mdetunilem8  20425  mdetunilem9  20426  maduval  20444  maducoeval  20445  maducoeval2  20446  madugsum  20449  madurid  20450  smadiadetglem2  20478  cramerimplem2  20490  mat2pmatghm  20535  mat2pmatmul  20536  m2cpminvid  20558  m2cpminvid2  20560  decpmatid  20575  decpmatmulsumfsupp  20578  monmatcollpw  20584  pmatcollpwscmatlem2  20595  mp2pm2mplem3  20613  mp2pm2mplem4  20614  pm2mpghm  20621  pm2mpmhmlem1  20623  ptval2  21404  cnmpt2t  21476  cnmpt22  21477  cnmptcom  21481  cnmptk2  21489  cnmpt2plusg  21892  istgp2  21895  prdstmdd  21927  cnmpt2vsca  21998  cnmpt2ds  22646  cnmpt2pc  22727  cnmpt2ip  23047  rrxds  23181  rrxmfval  23189  nvmfval  27499  mdetpmtr12  29891  madjusmdetlem1  29893  pstmval  29938  sseqval  30450  cvmlift2lem6  31290  cvmlift2lem7  31291  cvmlift2lem12  31296  matunitlindflem1  33405  dvhfvadd  36380  funcrngcsetcALT  41999