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

Theorem mpt2eq123dv 6344
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 465 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  E )
4 mpt2eq123dv.3 . . 3  |-  ( ph  ->  C  =  F )
54adantr 465 . 2  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  B ) )  ->  C  =  F )
61, 3, 5mpt2eq123dva 6343 1  |-  ( ph  ->  ( x  e.  A ,  y  e.  B  |->  C )  =  ( x  e.  D , 
y  e.  E  |->  F ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1383    e. wcel 1804    |-> cmpt2 6283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-oprab 6285  df-mpt2 6286
This theorem is referenced by:  mpt2eq123i  6345  bropopvvv  6865  prdsval  14834  imasval  14890  imasvscaval  14917  homffval  15068  homfeq  15071  comfffval  15075  comffval  15076  comfffval2  15078  comffval2  15079  comfeq  15083  oppcval  15090  monfval  15109  sectffval  15127  invffval  15134  cofuval  15230  natfval  15294  fucval  15306  fucco  15310  coafval  15370  setcval  15383  setcco  15389  catcval  15402  catcco  15407  xpcval  15425  xpchomfval  15427  xpccofval  15430  1stfval  15439  2ndfval  15442  prfval  15447  evlfval  15465  evlf2  15466  curfval  15471  hofval  15500  hof2fval  15503  plusffval  15856  grpsubfval  16071  grpsubpropd  16119  mulgfval  16122  mulgpropd  16154  symgval  16383  lsmfval  16637  pj1fval  16691  efgtf  16719  prdsmgp  17238  dvrfval  17312  scaffval  17509  psrval  17990  ipffval  18661  frlmip  18787  mamufval  18865  mvmulfval  19022  marrepfval  19040  marepvfval  19045  submafval  19059  submaval  19061  madufval  19117  minmar1fval  19126  mat2pmatfval  19202  cpm2mfval  19228  decpmatval0  19243  decpmatval  19244  pmatcollpw3lem  19262  xkoval  20066  xkopt  20134  xpstopnlem1  20288  submtmd  20581  blfvalps  20864  ishtpy  21450  isphtpy  21459  pcofval  21488  rrxip  21800  q1pval  22532  r1pval  22535  taylfval  22732  midf  24120  ismidb  24122  ttgval  24156  wlkon  24511  trlon  24520  pthon  24555  spthon  24562  is2wlkonot  24841  is2spthonot  24842  2wlkonot3v  24853  2spthonot3v  24854  grpodivfval  25222  gxfval  25237  dipfval  25590  qqhval  27933  sxval  28139  sitmval  28268  cndprobval  28350  mclsval  28901  rrnval  30299  eldiophb  30666  mendval  31108  estrcval  32596  estrcco  32602  rngcvalOLD  32644  rngccoOLD  32671  funcrngcsetcALT  32682  ringcvalOLD  32687  ringccoOLD  32731  lincop  32879  ldualset  34725  paddfval  35396  tgrpfset  36345  tgrpset  36346  erngfset  36400  erngset  36401  erngfset-rN  36408  erngset-rN  36409  dvafset  36605  dvaset  36606  dvhfset  36682  dvhset  36683  djaffvalN  36735  djafvalN  36736  djhffval  36998  djhfval  36999  hlhilset  37539
  Copyright terms: Public domain W3C validator