MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpt2eq123dv Unicode version

Theorem mpt2eq123dv 5926
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
StepHypRef Expression
1 mpt2eq123dv.1 . 2  |-  ( ph  ->  A  =  D )
2 mpt2eq123dv.2 . . 3  |-  ( ph  ->  B  =  E )
32adantr 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  E )
4 mpt2eq123dv.3 . . 3  |-  ( ph  ->  C  =  F )
54adantr 451 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  C  =  F )
61, 3, 5mpt2eq123dva 5925 1  |-  ( ph  ->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  D , 
y  e.  E  |->  F ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696    e. cmpt2 5876
This theorem is referenced by:  mpt2eq123i  5927  seqeq2  11066  seqeq3  11067  prdsval  13371  imasval  13430  imasvscaval  13456  homffval  13610  homfeq  13613  comfffval  13617  comffval  13618  comfffval2  13620  comffval2  13621  comfeq  13625  oppcval  13632  monfval  13651  sectffval  13669  invffval  13676  cofuval  13772  natfval  13836  fucval  13848  fucco  13852  coafval  13912  setcval  13925  setcco  13931  catcval  13944  catcco  13949  xpcval  13967  xpchomfval  13969  xpccofval  13972  1stfval  13981  2ndfval  13984  prfval  13989  evlfval  14007  evlf2  14008  curfval  14013  hofval  14042  hof2fval  14045  joinfval  14137  meetfval  14144  plusffval  14395  grpsubfval  14540  grpsubpropd  14582  mulgfval  14584  mulgpropd  14616  symgval  14787  lsmfval  14965  pj1fval  15019  efgtf  15047  prdsmgp  15409  dvrfval  15482  scaffval  15661  psrval  16126  ipffval  16568  xkoval  17298  xkopt  17365  xpstopnlem1  17516  submtmd  17803  blfval  17963  ishtpy  18486  isphtpy  18495  pcofval  18524  q1pval  19555  r1pval  19558  taylfval  19754  grpodivfval  20925  gxfval  20940  dipfval  21291  sxval  23536  cndprobval  23651  relexp0  24040  relexpsucr  24041  iscst1  25277  islimrs  25683  isaddrv  25749  sigadd  25752  issubcv  25773  ismulcv  25784  fnmulcv  25787  isdivcv2  25796  isder  25810  ishoma  25890  linevala2  26181  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  rrnval  26654  eldiophb  26939  mamufval  27546  mamuval  27547  mendval  27594  iswlkon  28332  trlon  28339  istrlon  28340  trlonprop  28341  pthon  28361  ldualset  29937  paddfval  30608  tgrpfset  31555  tgrpset  31556  erngfset  31610  erngset  31611  erngfset-rN  31618  erngset-rN  31619  dvafset  31815  dvaset  31816  dvhfset  31892  dvhset  31893  djaffvalN  31945  djafvalN  31946  djhffval  32208  djhfval  32209  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-oprab 5878  df-mpt2 5879
  Copyright terms: Public domain W3C validator