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

Theorem mpt2eq123dv 6128
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 452 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  E )
4 mpt2eq123dv.3 . . 3  |-  ( ph  ->  C  =  F )
54adantr 452 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  C  =  F )
61, 3, 5mpt2eq123dva 6127 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 359    = wceq 1652    e. wcel 1725    e. cmpt2 6075
This theorem is referenced by:  mpt2eq123i  6129  bropopvvv  6418  seqeq2  11319  seqeq3  11320  prdsval  13670  imasval  13729  imasvscaval  13755  homffval  13909  homfeq  13912  comfffval  13916  comffval  13917  comfffval2  13919  comffval2  13920  comfeq  13924  oppcval  13931  monfval  13950  sectffval  13968  invffval  13975  cofuval  14071  natfval  14135  fucval  14147  fucco  14151  coafval  14211  setcval  14224  setcco  14230  catcval  14243  catcco  14248  xpcval  14266  xpchomfval  14268  xpccofval  14271  1stfval  14280  2ndfval  14283  prfval  14288  evlfval  14306  evlf2  14307  curfval  14312  hofval  14341  hof2fval  14344  joinfval  14436  meetfval  14443  plusffval  14694  grpsubfval  14839  grpsubpropd  14881  mulgfval  14883  mulgpropd  14915  symgval  15086  lsmfval  15264  pj1fval  15318  efgtf  15346  prdsmgp  15708  dvrfval  15781  scaffval  15960  psrval  16421  ipffval  16871  xkoval  17611  xkopt  17679  xpstopnlem1  17833  submtmd  18126  blfvalps  18405  ishtpy  18989  isphtpy  18998  pcofval  19027  q1pval  20068  r1pval  20071  taylfval  20267  wlkon  21522  trlon  21532  pthon  21567  spthon  21574  grpodivfval  21822  gxfval  21837  dipfval  22190  qqhval  24350  sxval  24536  sitmval  24653  cndprobval  24683  relexp0  25121  relexpsucr  25122  rrnval  26527  eldiophb  26806  mamufval  27411  mamuval  27412  mendval  27459  is2wlkonot  28283  is2spthonot  28284  2wlkonot3v  28295  2spthonot3v  28296  ldualset  29860  paddfval  30531  tgrpfset  31478  tgrpset  31479  erngfset  31533  erngset  31534  erngfset-rN  31541  erngset-rN  31542  dvafset  31738  dvaset  31739  dvhfset  31815  dvhset  31816  djaffvalN  31868  djafvalN  31869  djhffval  32131  djhfval  32132  hlhilset  32672
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-oprab 6077  df-mpt2 6078
  Copyright terms: Public domain W3C validator