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

Theorem mpt2eq123dv 6068
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 6067 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 1649    e. wcel 1717    e. cmpt2 6015
This theorem is referenced by:  mpt2eq123i  6069  bropopvvv  6358  seqeq2  11247  seqeq3  11248  prdsval  13598  imasval  13657  imasvscaval  13683  homffval  13837  homfeq  13840  comfffval  13844  comffval  13845  comfffval2  13847  comffval2  13848  comfeq  13852  oppcval  13859  monfval  13878  sectffval  13896  invffval  13903  cofuval  13999  natfval  14063  fucval  14075  fucco  14079  coafval  14139  setcval  14152  setcco  14158  catcval  14171  catcco  14176  xpcval  14194  xpchomfval  14196  xpccofval  14199  1stfval  14208  2ndfval  14211  prfval  14216  evlfval  14234  evlf2  14235  curfval  14240  hofval  14269  hof2fval  14272  joinfval  14364  meetfval  14371  plusffval  14622  grpsubfval  14767  grpsubpropd  14809  mulgfval  14811  mulgpropd  14843  symgval  15014  lsmfval  15192  pj1fval  15246  efgtf  15274  prdsmgp  15636  dvrfval  15709  scaffval  15888  psrval  16349  ipffval  16795  xkoval  17533  xkopt  17601  xpstopnlem1  17755  submtmd  18048  blfval  18314  ishtpy  18861  isphtpy  18870  pcofval  18899  q1pval  19936  r1pval  19939  taylfval  20135  wlkon  21387  trlon  21397  pthon  21422  grpodivfval  21671  gxfval  21686  dipfval  22039  qqhval  24150  sxval  24333  cndprobval  24463  relexp0  24901  relexpsucr  24902  rrnval  26220  eldiophb  26499  mamufval  27105  mamuval  27106  mendval  27153  ldualset  29291  paddfval  29962  tgrpfset  30909  tgrpset  30910  erngfset  30964  erngset  30965  erngfset-rN  30972  erngset-rN  30973  dvafset  31169  dvaset  31170  dvhfset  31246  dvhset  31247  djaffvalN  31299  djafvalN  31300  djhffval  31562  djhfval  31563  hlhilset  32103
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-oprab 6017  df-mpt2 6018
  Copyright terms: Public domain W3C validator