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

Theorem mpteq12dv 4114
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 4113 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  C  |->  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    e. wcel 1696    e. cmpt 4093
This theorem is referenced by:  mpteq12i  4120  offval  6101  offval3  6107  cantnffval  7380  cnfcomlem  7418  fseqenlem1  7667  dfac12lem1  7785  dfac12r  7788  ackbij2lem2  7882  ackbij2lem3  7883  r1om  7886  wunex2  8376  wuncval2  8385  ccatfval  11444  swrdval  11466  revval  11494  revco  11505  ccatco  11506  odzval  12872  vdwpc  13043  restval  13347  prdsval  13371  imasval  13430  divsval  13460  mrcfval  13526  cidfval  13594  monfval  13651  ismon  13652  isepi  13659  idfuval  13766  resfval  13782  resfval2  13783  fucval  13848  fucco  13852  homafval  13877  idafval  13905  prfval  13989  prf2fval  13991  curfval  14013  curf1  14015  curf2  14019  curfpropd  14023  hofval  14042  hof2fval  14045  yonedalem3a  14064  yonedalem4a  14065  yonedalem4c  14067  yonedainv  14071  lubfval  14128  glbfval  14133  ipoval  14273  grpinvfval  14536  grpinvpropd  14559  cntzfval  14812  odfval  14864  sylow1lem2  14926  sylow1lem4  14928  sylow2blem1  14947  sylow3lem1  14954  sylow3lem2  14955  sylow3lem3  14956  sylow3lem6  14959  pj1fval  15019  vrgpfval  15091  gsum2d  15239  gsum2d2  15241  dprdval  15254  dprd2dlem2  15291  dprd2dlem1  15292  dprd2da  15293  dprd2d2  15295  dpjfval  15306  staffval  15628  lspfval  15746  lsppropd  15791  sraval  15945  aspval  16084  asclfval  16090  ressascl  16099  psrval  16126  psrass1lem  16139  psrmulval  16147  mvrfval  16181  opsrval  16232  coe1mul2  16362  isphl  16548  ocvfval  16582  pjfval  16622  ntrfval  16777  clsfval  16778  neifval  16852  lpfval  16886  ordtval  16935  ordtbas2  16937  ordtcnv  16947  ordtrest  16948  ordtrest2  16950  cnpfval  16980  kqval  17433  fmval  17654  fmf  17656  flffval  17700  fcfval  17744  tsmsval2  17828  nmfval  18127  nmpropd  18132  nmpropd2  18133  subgnm  18165  tngnm  18183  nmofval  18239  pi1xfrcnv  18571  iscph  18622  tchval  18666  limcfval  19238  dvfval  19263  eldv  19264  mpfrcl  19418  evlsval  19419  evl1fval  19426  mdegfval  19464  mdegmullem  19480  mdegpropd  19486  coe1mul3  19501  ig1pval  19574  taylfval  19754  grpoinvfval  20907  nmoofval  21356  eigvalfval  22493  ofcfval  23474  ofcfval3  23478  ofcfval4  23481  indv  23611  cvmliftlem5  23835  cvmliftlem15  23844  vdgrfval  23904  cur1val  25301  islimrs  25683  isaddrv  25749  isnullcv  25755  valvze  25757  isucv  25780  ismulcv  25784  isder  25810  cinvlem1  25931  isntr  25976  islimcat  25979  isgraphmrph  26026  domcatfun  26028  domcatval  26033  codcatfun  26037  codcatval  26039  isconc1  26109  isconc2  26110  isconc3  26111  clscnc  26113  isside0  26267  aishp  26275  tailfval  26424  uvcfval  27336  hbtlem1  27430  hbtlem7  27432  rgspnval  27476  pmtrfval  27496  psgnfval  27526  mamufval  27546  mdetfval  27590  cytpval  27631  lsatset  29802  lkrfval  29899  pmapfval  30567  pclfvalN  30700  polfvalN  30715  watfvalN  30803  ldilfset  30919  ltrnfset  30928  dilfsetN  30963  trnfsetN  30966  trlfset  30971  trlset  30972  tgrpfset  31555  tendofset  31569  erngfset  31610  erngset  31611  erngfset-rN  31618  erngset-rN  31619  dvafset  31815  diaffval  31842  diafval  31843  dvhfset  31892  dvhset  31893  docaffvalN  31933  docafvalN  31934  djaffvalN  31945  dibffval  31952  dibfval  31953  dicffval  31986  dicfval  31987  dihffval  32042  dochffval  32161  dochfval  32162  djhffval  32208  lcdfval  32400  mapdffval  32438  mapdfval  32439  hvmapffval  32570  hvmapfval  32571  hdmap1ffval  32608  hdmap1fval  32609  hdmapffval  32641  hdmapfval  32642  hgmapffval  32700  hgmapfval  32701  hlhilset  32749
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-opab 4094  df-mpt 4095
  Copyright terms: Public domain W3C validator