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

Theorem mpt2eq123dv 5910
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 5909 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 1623    e. wcel 1684    e. cmpt2 5860
This theorem is referenced by:  mpt2eq123i  5911  seqeq2  11050  seqeq3  11051  prdsval  13355  imasval  13414  imasvscaval  13440  homffval  13594  homfeq  13597  comfffval  13601  comffval  13602  comfffval2  13604  comffval2  13605  comfeq  13609  oppcval  13616  monfval  13635  sectffval  13653  invffval  13660  cofuval  13756  natfval  13820  fucval  13832  fucco  13836  coafval  13896  setcval  13909  setcco  13915  catcval  13928  catcco  13933  xpcval  13951  xpchomfval  13953  xpccofval  13956  1stfval  13965  2ndfval  13968  prfval  13973  evlfval  13991  evlf2  13992  curfval  13997  hofval  14026  hof2fval  14029  joinfval  14121  meetfval  14128  plusffval  14379  grpsubfval  14524  grpsubpropd  14566  mulgfval  14568  mulgpropd  14600  symgval  14771  lsmfval  14949  pj1fval  15003  efgtf  15031  prdsmgp  15393  dvrfval  15466  scaffval  15645  psrval  16110  ipffval  16552  xkoval  17282  xkopt  17349  xpstopnlem1  17500  submtmd  17787  blfval  17947  ishtpy  18470  isphtpy  18479  pcofval  18508  q1pval  19539  r1pval  19542  taylfval  19738  grpodivfval  20909  gxfval  20924  dipfval  21275  sxval  23521  cndprobval  23636  relexp0  24025  relexpsucr  24026  iscst1  25174  islimrs  25580  isaddrv  25646  sigadd  25649  issubcv  25670  ismulcv  25681  fnmulcv  25684  isdivcv2  25693  isder  25707  ishoma  25787  linevala2  26078  sgplpte21  26132  sgplpte22  26138  isray2  26153  isray  26154  rrnval  26551  eldiophb  26836  mamufval  27443  mamuval  27444  mendval  27491  ldualset  29315  paddfval  29986  tgrpfset  30933  tgrpset  30934  erngfset  30988  erngset  30989  erngfset-rN  30996  erngset-rN  30997  dvafset  31193  dvaset  31194  dvhfset  31270  dvhset  31271  djaffvalN  31323  djafvalN  31324  djhffval  31586  djhfval  31587  hlhilset  32127
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-oprab 5862  df-mpt2 5863
  Copyright terms: Public domain W3C validator