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

Theorem mpteq12dv 4098
Description: An equality inference for the maps to notation. (Contributed by NM, 24-Aug-2011.) (Revised by Mario Carneiro, 16-Dec-2013.)
Hypotheses
Ref Expression
mpteq12dv.1  |-  ( ph  ->  A  =  C )
mpteq12dv.2  |-  ( ph  ->  B  =  D )
Assertion
Ref Expression
mpteq12dv  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Distinct variable group:    ph, x
Allowed substitution hints:    A( x)    B( x)    C( x)    D( x)

Proof of Theorem mpteq12dv
StepHypRef Expression
1 mpteq12dv.1 . 2  |-  ( ph  ->  A  =  C )
2 mpteq12dv.2 . . 3  |-  ( ph  ->  B  =  D )
32adantr 451 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  D )
41, 3mpteq12dva 4097 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684    e. cmpt 4077
This theorem is referenced by:  mpteq12i  4104  offval  6085  offval3  6091  cantnffval  7364  cnfcomlem  7402  fseqenlem1  7651  dfac12lem1  7769  dfac12r  7772  ackbij2lem2  7866  ackbij2lem3  7867  r1om  7870  wunex2  8360  wuncval2  8369  ccatfval  11428  swrdval  11450  revval  11478  revco  11489  ccatco  11490  odzval  12856  vdwpc  13027  restval  13331  prdsval  13355  imasval  13414  divsval  13444  mrcfval  13510  cidfval  13578  monfval  13635  ismon  13636  isepi  13643  idfuval  13750  resfval  13766  resfval2  13767  fucval  13832  fucco  13836  homafval  13861  idafval  13889  prfval  13973  prf2fval  13975  curfval  13997  curf1  13999  curf2  14003  curfpropd  14007  hofval  14026  hof2fval  14029  yonedalem3a  14048  yonedalem4a  14049  yonedalem4c  14051  yonedainv  14055  lubfval  14112  glbfval  14117  ipoval  14257  grpinvfval  14520  grpinvpropd  14543  cntzfval  14796  odfval  14848  sylow1lem2  14910  sylow1lem4  14912  sylow2blem1  14931  sylow3lem1  14938  sylow3lem2  14939  sylow3lem3  14940  sylow3lem6  14943  pj1fval  15003  vrgpfval  15075  gsum2d  15223  gsum2d2  15225  dprdval  15238  dprd2dlem2  15275  dprd2dlem1  15276  dprd2da  15277  dprd2d2  15279  dpjfval  15290  staffval  15612  lspfval  15730  lsppropd  15775  sraval  15929  aspval  16068  asclfval  16074  ressascl  16083  psrval  16110  psrass1lem  16123  psrmulval  16131  mvrfval  16165  opsrval  16216  coe1mul2  16346  isphl  16532  ocvfval  16566  pjfval  16606  ntrfval  16761  clsfval  16762  neifval  16836  lpfval  16870  ordtval  16919  ordtbas2  16921  ordtcnv  16931  ordtrest  16932  ordtrest2  16934  cnpfval  16964  kqval  17417  fmval  17638  fmf  17640  flffval  17684  fcfval  17728  tsmsval2  17812  nmfval  18111  nmpropd  18116  nmpropd2  18117  subgnm  18149  tngnm  18167  nmofval  18223  pi1xfrcnv  18555  iscph  18606  tchval  18650  limcfval  19222  dvfval  19247  eldv  19248  mpfrcl  19402  evlsval  19403  evl1fval  19410  mdegfval  19448  mdegmullem  19464  mdegpropd  19470  coe1mul3  19485  ig1pval  19558  taylfval  19738  grpoinvfval  20891  nmoofval  21340  eigvalfval  22477  ofcfval  23459  ofcfval3  23463  ofcfval4  23466  indv  23596  cvmliftlem5  23820  cvmliftlem15  23829  vdgrfval  23889  cur1val  25198  islimrs  25580  isaddrv  25646  isnullcv  25652  valvze  25654  isucv  25677  ismulcv  25681  isder  25707  cinvlem1  25828  isntr  25873  islimcat  25876  isgraphmrph  25923  domcatfun  25925  domcatval  25930  codcatfun  25934  codcatval  25936  isconc1  26006  isconc2  26007  isconc3  26008  clscnc  26010  isside0  26164  aishp  26172  tailfval  26321  uvcfval  27233  hbtlem1  27327  hbtlem7  27329  rgspnval  27373  pmtrfval  27393  psgnfval  27423  mamufval  27443  mdetfval  27487  cytpval  27528  lsatset  29180  lkrfval  29277  pmapfval  29945  pclfvalN  30078  polfvalN  30093  watfvalN  30181  ldilfset  30297  ltrnfset  30306  dilfsetN  30341  trnfsetN  30344  trlfset  30349  trlset  30350  tgrpfset  30933  tendofset  30947  erngfset  30988  erngset  30989  erngfset-rN  30996  erngset-rN  30997  dvafset  31193  diaffval  31220  diafval  31221  dvhfset  31270  dvhset  31271  docaffvalN  31311  docafvalN  31312  djaffvalN  31323  dibffval  31330  dibfval  31331  dicffval  31364  dicfval  31365  dihffval  31420  dochffval  31539  dochfval  31540  djhffval  31586  lcdfval  31778  mapdffval  31816  mapdfval  31817  hvmapffval  31948  hvmapfval  31949  hdmap1ffval  31986  hdmap1fval  31987  hdmapffval  32019  hdmapfval  32020  hgmapffval  32078  hgmapfval  32079  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-ral 2548  df-opab 4078  df-mpt 4079
  Copyright terms: Public domain W3C validator