Theorem mpt2eq123dv 6258

Description: An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.)

Hypotheses

Ref	Expression
mpt2eq123dv.1	|- ( ph -> A = D )
mpt2eq123dv.2	|- ( ph -> B = E )
mpt2eq123dv.3	|- ( ph -> C = F )

Assertion

Ref	Expression
mpt2eq123dv	|- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )

Distinct variable groups:   ph, x   ph, y

Allowed substitution hints:   A( x, y)   B( x, y)   C( x, y)   D( x, y)   E( x, y)   F( x, y)

Proof of Theorem mpt2eq123dv

Step	Hyp	Ref	Expression
1		mpt2eq123dv.1	. 2 |- ( ph -> A = D )
2		mpt2eq123dv.2	. . 3 |- ( ph -> B = E )
3	2	adantr 463	. 2 |- ( ( ph /\ x e. A ) -> B = E )
4		mpt2eq123dv.3	. . 3 |- ( ph -> C = F )
5	4	adantr 463	. 2 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = F )
6	1, 3, 5	mpt2eq123dva 6257	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )

Syntax hints:   -> wi 4   /\ wa 367   = wceq 1399   e. wcel 1826   |-> cmpt2 6198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-oprab 6200  df-mpt2 6201

This theorem is referenced by:  mpt2eq123i  6259  bropopvvv  6779  prdsval  14862  imasval  14918  imasvscaval  14945  homffval  15096  homfeq  15100  comfffval  15104  comffval  15105  comfffval2  15107  comffval2  15108  comfeq  15112  oppcval  15119  monfval  15138  sectffval  15156  invffval  15164  isofn  15181  cofuval  15288  natfval  15352  fucval  15364  fucco  15368  coafval  15460  setcval  15473  setcco  15479  catcval  15492  catcco  15497  estrcval  15510  estrcco  15516  xpcval  15563  xpchomfval  15565  xpccofval  15568  1stfval  15577  2ndfval  15580  prfval  15585  evlfval  15603  evlf2  15604  curfval  15609  hofval  15638  hof2fval  15641  plusffval  15994  grpsubfval  16209  grpsubpropd  16257  mulgfval  16260  mulgpropd  16292  symgval  16521  lsmfval  16775  pj1fval  16829  efgtf  16857  prdsmgp  17372  dvrfval  17446  scaffval  17643  psrval  18124  ipffval  18774  frlmip  18898  mamufval  18972  mvmulfval  19129  marrepfval  19147  marepvfval  19152  submafval  19166  submaval  19168  madufval  19224  minmar1fval  19233  mat2pmatfval  19309  cpm2mfval  19335  decpmatval0  19350  decpmatval  19351  pmatcollpw3lem  19369  xkoval  20173  xkopt  20241  xpstopnlem1  20395  submtmd  20688  blfvalps  20971  ishtpy  21557  isphtpy  21566  pcofval  21595  rrxip  21907  q1pval  22639  r1pval  22642  taylfval  22839  midf  24262  ismidb  24264  ttgval  24299  wlkon  24654  trlon  24663  pthon  24698  spthon  24705  is2wlkonot  24984  is2spthonot  24985  2wlkonot3v  24996  2spthonot3v  24997  grpodivfval  25361  gxfval  25376  dipfval  25729  qqhval  28108  sxval  28317  sitmval  28473  cndprobval  28555  mclsval  29112  rrnval  30489  eldiophb  30855  mendval  31300  rngcvalALTV  32969  rngccoALTV  32996  funcrngcsetcALT  33007  ringcvalALTV  33015  ringccoALTV  33059  lincop  33209  ldualset  35263  paddfval  35934  tgrpfset  36883  tgrpset  36884  erngfset  36938  erngset  36939  erngfset-rN  36946  erngset-rN  36947  dvafset  37143  dvaset  37144  dvhfset  37220  dvhset  37221  djaffvalN  37273  djafvalN  37274  djhffval  37536  djhfval  37537  hlhilset  38077