Theorem mpt2eq3dva 6141

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 1183	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3	2	eqeq2d 2446	. . . 4 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> ( z = C <-> z = D ) )
4	3	pm5.32da 636	. . 3 |- ( ph -> ( ( ( x e. A /\ y e. B ) /\ z = C ) <-> ( ( x e. A /\ y e. B ) /\ z = D ) ) )
5	4	oprabbidv 6131	. 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 6087	. 2 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7		df-mpt2 6087	. 2 |- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8	5, 6, 7	3eqtr4g 2492	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. A , y e. B |-> D ) )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 960   = wceq 1364   e. wcel 1757   {coprab 6083   e. cmpt2 6084

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-clab 2422  df-cleq 2428  df-oprab 6086  df-mpt2 6087

This theorem is referenced by:  mpt2eq3ia  6142  mpt2eq3dv  6143  ofeq  6313  fmpt2co  6647  seqomeq12  6897  mapxpen  7467  cantnffval  7859  cantnfres  7875  cantnfvalOLD  7896  sadfval  13633  smufval  13658  vdwapfval  14017  comfeq  14630  monpropd  14661  cofuval2  14782  cofuass  14784  cofulid  14785  cofurid  14786  catcisolem  14959  prfval  14994  prf1st  14999  prf2nd  15000  1st2ndprf  15001  xpcpropd  15003  curf1  15020  curfuncf  15033  curf2ndf  15042  grpsubpropd2  15609  mulgpropd  15642  lsmfval  16119  oppglsm  16123  subglsm  16152  lsmpropd  16156  gsumcom2  16443  gsumdixpOLD  16637  gsumdixp  16638  psrvscafval  17397  evlslem4OLD  17520  evlslem4  17521  evlslem2  17527  psrplusgpropd  17590  mamures  18134  mamutpos  18187  1marepvmarrepid  18230  1marepvsma1  18238  mdetrsca2  18255  mdetrlin2  18257  mdetunilem5  18266  mdetunilem6  18267  mdetunilem7  18268  mdetunilem8  18269  mdetunilem9  18270  madufval  18287  maduval  18288  maducoeval  18289  maducoeval2  18290  madugsum  18293  madurid  18294  smadiadetglem2  18322  cramerimplem2  18334  ptval2  19018  cnmpt2t  19090  cnmpt22  19091  cnmptcom  19095  cnmptk2  19103  cnmpt2plusg  19503  istgp2  19506  prdstmdd  19538  cnmpt2vsca  19613  cnmpt2ds  20264  cnmpt2pc  20344  cnmpt2ip  20604  rrxds  20741  rrxmfval  20749  ttgval  22946  nvmfval  23849  pstmval  26178  ofceq  26395  sseqval  26621  cvmlift2lem6  27047  cvmlift2lem7  27048  cvmlift2lem12  27053  dmatmul  30667  dmatcrng  30672  scmatcrng  30679  dvhfvadd  34349