Theorem mpt2eq123dv 6147

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

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1364   e. wcel 1761   e. cmpt2 6092

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 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-oprab 6094  df-mpt2 6095

This theorem is referenced by:  mpt2eq123i  6148  bropopvvv  6652  seqeq2  11806  seqeq3  11807  prdsval  14389  imasval  14445  imasvscaval  14472  homffval  14626  homfeq  14629  comfffval  14633  comffval  14634  comfffval2  14636  comffval2  14637  comfeq  14641  oppcval  14648  monfval  14667  sectffval  14685  invffval  14692  cofuval  14788  natfval  14852  fucval  14864  fucco  14868  coafval  14928  setcval  14941  setcco  14947  catcval  14960  catcco  14965  xpcval  14983  xpchomfval  14985  xpccofval  14988  1stfval  14997  2ndfval  15000  prfval  15005  evlfval  15023  evlf2  15024  curfval  15029  hofval  15058  hof2fval  15061  plusffval  15423  grpsubfval  15573  grpsubpropd  15619  mulgfval  15621  mulgpropd  15653  symgval  15877  lsmfval  16130  pj1fval  16184  efgtf  16212  prdsmgp  16692  dvrfval  16766  scaffval  16946  psrval  17407  ipffval  18036  frlmip  18162  mamufval  18242  mamuval  18243  mvmulfval  18312  marrepfval  18330  marepvfval  18335  submafval  18349  submaval  18351  madufval  18402  minmar1fval  18411  xkoval  19119  xkopt  19187  xpstopnlem1  19341  submtmd  19634  blfvalps  19917  ishtpy  20503  isphtpy  20512  pcofval  20541  rrxip  20853  q1pval  21584  r1pval  21587  taylfval  21783  ttgval  23056  wlkon  23364  trlon  23374  pthon  23409  spthon  23416  grpodivfval  23664  gxfval  23679  dipfval  24032  qqhval  26339  sxval  26540  sitmval  26664  cndprobval  26746  relexp0  27260  relexpsucr  27261  rrnval  28651  eldiophb  29020  mendval  29465  is2wlkonot  30307  is2spthonot  30308  2wlkonot3v  30319  2spthonot3v  30320  lincop  30783  ldualset  32492  paddfval  33163  tgrpfset  34110  tgrpset  34111  erngfset  34165  erngset  34166  erngfset-rN  34173  erngset-rN  34174  dvafset  34370  dvaset  34371  dvhfset  34447  dvhset  34448  djaffvalN  34500  djafvalN  34501  djhffval  34763  djhfval  34764  hlhilset  35304