Theorem mpt2eq123dv 6163

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 465	. 2 |- ( ( ph /\ x e. A ) -> B = E )
4		mpt2eq123dv.3	. . 3 |- ( ph -> C = F )
5	4	adantr 465	. 2 |- ( ( ph /\ ( x e. A /\ y e. B ) ) -> C = F )
6	1, 3, 5	mpt2eq123dva 6162	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1369   e. wcel 1756   e. cmpt2 6108

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 2423

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-oprab 6110  df-mpt2 6111

This theorem is referenced by:  mpt2eq123i  6164  bropopvvv  6668  seqeq2  11825  seqeq3  11826  prdsval  14408  imasval  14464  imasvscaval  14491  homffval  14645  homfeq  14648  comfffval  14652  comffval  14653  comfffval2  14655  comffval2  14656  comfeq  14660  oppcval  14667  monfval  14686  sectffval  14704  invffval  14711  cofuval  14807  natfval  14871  fucval  14883  fucco  14887  coafval  14947  setcval  14960  setcco  14966  catcval  14979  catcco  14984  xpcval  15002  xpchomfval  15004  xpccofval  15007  1stfval  15016  2ndfval  15019  prfval  15024  evlfval  15042  evlf2  15043  curfval  15048  hofval  15077  hof2fval  15080  plusffval  15442  grpsubfval  15595  grpsubpropd  15641  mulgfval  15643  mulgpropd  15675  symgval  15899  lsmfval  16152  pj1fval  16206  efgtf  16234  prdsmgp  16717  dvrfval  16791  scaffval  16981  psrval  17444  ipffval  18092  frlmip  18218  mamufval  18298  mamuval  18299  mvmulfval  18368  marrepfval  18386  marepvfval  18391  submafval  18405  submaval  18407  madufval  18458  minmar1fval  18467  xkoval  19175  xkopt  19243  xpstopnlem1  19397  submtmd  19690  blfvalps  19973  ishtpy  20559  isphtpy  20568  pcofval  20597  rrxip  20909  q1pval  21640  r1pval  21643  taylfval  21839  ttgval  23136  wlkon  23444  trlon  23454  pthon  23489  spthon  23496  grpodivfval  23744  gxfval  23759  dipfval  24112  qqhval  26418  sxval  26619  sitmval  26749  cndprobval  26831  relexp0  27346  relexpsucr  27347  rrnval  28745  eldiophb  29114  mendval  29559  is2wlkonot  30401  is2spthonot  30402  2wlkonot3v  30413  2spthonot3v  30414  lincop  30961  ldualset  32789  paddfval  33460  tgrpfset  34407  tgrpset  34408  erngfset  34462  erngset  34463  erngfset-rN  34470  erngset-rN  34471  dvafset  34667  dvaset  34668  dvhfset  34744  dvhset  34745  djaffvalN  34797  djafvalN  34798  djhffval  35060  djhfval  35061  hlhilset  35601