Theorem mpt2eq123dv 6095

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

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   e. cmpt2 6042

This theorem is referenced by:  mpt2eq123i  6096  bropopvvv  6385  seqeq2  11282  seqeq3  11283  prdsval  13633  imasval  13692  imasvscaval  13718  homffval  13872  homfeq  13875  comfffval  13879  comffval  13880  comfffval2  13882  comffval2  13883  comfeq  13887  oppcval  13894  monfval  13913  sectffval  13931  invffval  13938  cofuval  14034  natfval  14098  fucval  14110  fucco  14114  coafval  14174  setcval  14187  setcco  14193  catcval  14206  catcco  14211  xpcval  14229  xpchomfval  14231  xpccofval  14234  1stfval  14243  2ndfval  14246  prfval  14251  evlfval  14269  evlf2  14270  curfval  14275  hofval  14304  hof2fval  14307  joinfval  14399  meetfval  14406  plusffval  14657  grpsubfval  14802  grpsubpropd  14844  mulgfval  14846  mulgpropd  14878  symgval  15049  lsmfval  15227  pj1fval  15281  efgtf  15309  prdsmgp  15671  dvrfval  15744  scaffval  15923  psrval  16384  ipffval  16834  xkoval  17572  xkopt  17640  xpstopnlem1  17794  submtmd  18087  blfvalps  18366  ishtpy  18950  isphtpy  18959  pcofval  18988  q1pval  20029  r1pval  20032  taylfval  20228  wlkon  21483  trlon  21493  pthon  21528  spthon  21535  grpodivfval  21783  gxfval  21798  dipfval  22151  qqhval  24311  sxval  24497  sitmval  24614  cndprobval  24644  relexp0  25082  relexpsucr  25083  rrnval  26426  eldiophb  26705  mamufval  27311  mamuval  27312  mendval  27359  is2wlkonot  28060  is2spthonot  28061  2wlkonot3v  28072  2spthonot3v  28073  ldualset  29608  paddfval  30279  tgrpfset  31226  tgrpset  31227  erngfset  31281  erngset  31282  erngfset-rN  31289  erngset-rN  31290  dvafset  31486  dvaset  31487  dvhfset  31563  dvhset  31564  djaffvalN  31616  djafvalN  31617  djhffval  31879  djhfval  31880  hlhilset  32420

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-oprab 6044  df-mpt2 6045