Theorem mpt2eq3dva 6145

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 1188	. . . . 5 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = D )
3	2	eqeq2d 2449	. . . 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 6135	. 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 6091	. 2 |- ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
7		df-mpt2 6091	. 2 |- ( x e. A , y e. B |-> D ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = D ) }
8	5, 6, 7	3eqtr4g 2495	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 1369   e. wcel 1756   {coprab 6087   e. cmpt2 6088

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-oprab 6090  df-mpt2 6091

This theorem is referenced by:  mpt2eq3ia  6146  mpt2eq3dv  6147  ofeq  6317  fmpt2co  6651  seqomeq12  6901  mapxpen  7469  cantnffval  7861  cantnfres  7877  cantnfvalOLD  7898  sadfval  13640  smufval  13665  vdwapfval  14024  comfeq  14637  monpropd  14668  cofuval2  14789  cofuass  14791  cofulid  14792  cofurid  14793  catcisolem  14966  prfval  15001  prf1st  15006  prf2nd  15007  1st2ndprf  15008  xpcpropd  15010  curf1  15027  curfuncf  15040  curf2ndf  15049  grpsubpropd2  15618  mulgpropd  15651  lsmfval  16128  oppglsm  16132  subglsm  16161  lsmpropd  16165  gsumcom2  16455  gsumdixpOLD  16688  gsumdixp  16689  psrvscafval  17438  evlslem4OLD  17565  evlslem4  17566  evlslem2  17572  psrplusgpropd  17665  mamures  18265  mamutpos  18318  1marepvmarrepid  18361  1marepvsma1  18369  mdetrsca2  18386  mdetrlin2  18388  mdetunilem5  18397  mdetunilem6  18398  mdetunilem7  18399  mdetunilem8  18400  mdetunilem9  18401  madufval  18418  maduval  18419  maducoeval  18420  maducoeval2  18421  madugsum  18424  madurid  18425  smadiadetglem2  18453  cramerimplem2  18465  ptval2  19149  cnmpt2t  19221  cnmpt22  19222  cnmptcom  19226  cnmptk2  19234  cnmpt2plusg  19634  istgp2  19637  prdstmdd  19669  cnmpt2vsca  19744  cnmpt2ds  20395  cnmpt2pc  20475  cnmpt2ip  20735  rrxds  20872  rrxmfval  20880  ttgval  23072  nvmfval  23975  pstmval  26274  ofceq  26491  sseqval  26723  cvmlift2lem6  27149  cvmlift2lem7  27150  cvmlift2lem12  27155  dmatmul  30799  dmatcrng  30804  scmatcrng  30811  dvhfvadd  34576