Theorem mpt2eq123dv 6341

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 6340	1 |- ( ph -> ( x e. A , y e. B |-> C ) = ( x e. D , y e. E |-> F ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1379   e. wcel 1767   |-> cmpt2 6284

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-oprab 6286  df-mpt2 6287

This theorem is referenced by:  mpt2eq123i  6342  bropopvvv  6860  seqeq2  12075  seqeq3  12076  prdsval  14706  imasval  14762  imasvscaval  14789  homffval  14943  homfeq  14946  comfffval  14950  comffval  14951  comfffval2  14953  comffval2  14954  comfeq  14958  oppcval  14965  monfval  14984  sectffval  15002  invffval  15009  cofuval  15105  natfval  15169  fucval  15181  fucco  15185  coafval  15245  setcval  15258  setcco  15264  catcval  15277  catcco  15282  xpcval  15300  xpchomfval  15302  xpccofval  15305  1stfval  15314  2ndfval  15317  prfval  15322  evlfval  15340  evlf2  15341  curfval  15346  hofval  15375  hof2fval  15378  plusffval  15740  grpsubfval  15893  grpsubpropd  15941  mulgfval  15943  mulgpropd  15975  symgval  16199  lsmfval  16454  pj1fval  16508  efgtf  16536  prdsmgp  17043  dvrfval  17117  scaffval  17313  psrval  17782  ipffval  18450  frlmip  18576  mamufval  18654  mamuval  18655  mvmulfval  18811  marrepfval  18829  marepvfval  18834  submafval  18848  submaval  18850  madufval  18906  minmar1fval  18915  mat2pmatfval  18991  cpm2mfval  19017  decpmatval0  19032  decpmatval  19033  pmatcollpw3lem  19051  xkoval  19823  xkopt  19891  xpstopnlem1  20045  submtmd  20338  blfvalps  20621  ishtpy  21207  isphtpy  21216  pcofval  21245  rrxip  21557  q1pval  22289  r1pval  22292  taylfval  22488  ttgval  23854  wlkon  24209  trlon  24218  pthon  24253  spthon  24260  is2wlkonot  24539  is2spthonot  24540  2wlkonot3v  24551  2spthonot3v  24552  grpodivfval  24920  gxfval  24935  dipfval  25288  qqhval  27591  sxval  27801  sitmval  27930  cndprobval  28012  relexp0  28527  relexpsucr  28528  rrnval  29926  eldiophb  30294  mendval  30737  lincop  32082  ldualset  33922  paddfval  34593  tgrpfset  35540  tgrpset  35541  erngfset  35595  erngset  35596  erngfset-rN  35603  erngset-rN  35604  dvafset  35800  dvaset  35801  dvhfset  35877  dvhset  35878  djaffvalN  35930  djafvalN  35931  djhffval  36193  djhfval  36194  hlhilset  36734