Theorem mpt2eq123dv 6717

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

Syntax hints:   -> wi 4   /\ wa 384   = wceq 1483   e. wcel 1990   |-> cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-oprab 6654  df-mpt2 6655

This theorem is referenced by:  mpt2eq123i  6718  mptmpt2opabbrd  7248  el2mpt2csbcl  7250  bropopvvv  7255  bropfvvvv  7257  prdsval  16115  imasval  16171  imasvscaval  16198  homffval  16350  homfeq  16354  comfffval  16358  comffval  16359  comfffval2  16361  comffval2  16362  comfeq  16366  oppcval  16373  monfval  16392  sectffval  16410  invffval  16418  isofn  16435  cofuval  16542  natfval  16606  fucval  16618  fucco  16622  coafval  16714  setcval  16727  setcco  16733  catcval  16746  catcco  16751  estrcval  16764  estrcco  16770  xpcval  16817  xpchomfval  16819  xpccofval  16822  1stfval  16831  2ndfval  16834  prfval  16839  evlfval  16857  evlf2  16858  curfval  16863  hofval  16892  hof2fval  16895  plusffval  17247  grpsubfval  17464  grpsubpropd  17520  mulgfval  17542  mulgpropd  17584  symgval  17799  lsmfval  18053  pj1fval  18107  efgtf  18135  prdsmgp  18610  dvrfval  18684  scaffval  18881  psrval  19362  ipffval  19993  phssip  20003  frlmip  20117  mamufval  20191  mvmulfval  20348  marrepfval  20366  marepvfval  20371  submafval  20385  submaval  20387  madufval  20443  minmar1fval  20452  mat2pmatfval  20528  cpm2mfval  20554  decpmatval0  20569  decpmatval  20570  pmatcollpw3lem  20588  xkoval  21390  xkopt  21458  xpstopnlem1  21612  submtmd  21908  blfvalps  22188  ishtpy  22771  isphtpy  22780  pcofval  22810  rrxip  23178  q1pval  23913  r1pval  23916  taylfval  24113  midf  25668  ismidb  25670  ttgval  25755  wwlksnon  26738  wspthsnon  26739  grpodivfval  27388  dipfval  27557  submatres  29872  lmatval  29879  lmatcl  29882  qqhval  30018  sxval  30253  sitmval  30411  cndprobval  30495  mclsval  31460  csbfinxpg  33225  rrnval  33626  ldualset  34412  paddfval  35083  tgrpfset  36032  tgrpset  36033  erngfset  36087  erngset  36088  erngfset-rN  36095  erngset-rN  36096  dvafset  36292  dvaset  36293  dvhfset  36369  dvhset  36370  djaffvalN  36422  djafvalN  36423  djhffval  36685  djhfval  36686  hlhilset  37226  eldiophb  37320  mendval  37753  hoidmvval  40791  ovnhoi  40817  hspval  40823  hspmbllem2  40841  hoimbl  40845  rngcvalALTV  41961  rngccoALTV  41988  funcrngcsetcALT  41999  ringcvalALTV  42007  ringccoALTV  42051  lincop  42197