MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq1d Structured version   Visualization version   GIF version

Theorem mpteq1d 4890
Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)
Hypothesis
Ref Expression
mpteq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
mpteq1d (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵
Allowed substitution hints:   𝜑(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq1d
StepHypRef Expression
1 mpteq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 mpteq1 4889 . 2 (𝐴 = 𝐵 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝑥𝐴𝐶) = (𝑥𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  cmpt 4881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-ral 3055  df-opab 4865  df-mpt 4882
This theorem is referenced by:  csbmpt2  5161  fmptapd  6601  offval  7069  mpt2sn  7436  mpt2curryd  7564  cantnff  8744  dfac12lem1  9157  ackbij2lem2  9254  swrd00  13617  swrd0val  13620  swrdlend  13631  swrd0  13634  repswswrd  13731  repswrevw  13733  revco  13780  ccatco  13781  ofccat  13909  vdwapfval  15877  imasdsval  16377  mrcfval  16470  catidd  16542  curfpropd  17074  pwspjmhm  17569  grpinvfval  17661  psgnfval  18120  psgnfvalfi  18133  odfval  18152  frgpup3lem  18390  gsum2d2  18573  gsumxp  18575  telgsumfzs  18586  dprd2d2  18643  srgbinom  18745  gsummgp0  18808  pwsco1rhm  18940  pwsco2rhm  18941  staffval  19049  asclfval  19536  asclpropd  19548  mpfrcl  19720  evlsval  19721  evls1rhmlem  19888  evl1fval  19894  phlpropd  20202  pjfval  20252  mvmulfval  20550  submafval  20587  mdetfval  20594  nfimdetndef  20597  mdetfval1  20598  mdet0pr  20600  m1detdiag  20605  madufval  20645  minmar1fval  20654  gsummatr01  20667  pmatcollpw3fi1lem2  20794  pmatcollpw3fi1  20795  cpmadugsumlemF  20883  ispnrm  21345  ptval2  21606  ptpjcn  21616  xkoptsub  21659  kqval  21731  pt1hmeo  21811  fmval  21948  tmdgsum  22100  subgtgp  22110  prdstmdd  22128  prdsxmslem2  22535  nmfval  22594  lebnumlem1  22961  limcmpt2  23847  dvcmulf  23907  mdegfval  24021  ulmshft  24343  wwlksnextbij  27020  off2  29752  gsummpt2co  30089  esumnul  30419  ofcfval4  30476  measdivcst  30597  omsfval  30665  signstfval  30950  signstf0  30954  signstfvn  30955  mrsubffval  31711  mrsubfval  31712  msubfval  31728  elmsubrn  31732  mvhfval  31737  msrfval  31741  fwddifval  32575  tailfval  32673  curf  33700  poimirlem24  33746  ftc1anc  33806  sdclem2  33851  erngfset  36589  erngfset-rN  36597  dvhfset  36871  dvhset  36872  mzpclval  37790  mzpcompact2  37817  fsovrfovd  38805  mptima2  39956  supcnvlimsupmpt  40476  cncfshiftioo  40608  cncfiooicc  40610  dvsinax  40630  iblspltprt  40692  itgspltprt  40698  itgiccshift  40699  dirkercncflem2  40824  fourierdlem90  40916  fourierdlem92  40918  sge0val  41086  sge0prle  41121  sge0ss  41132  sge0iunmptlemfi  41133  sge0p1  41134  sge0iunmptlemre  41135  sge0iunmpt  41138  sge0xp  41149  ismeannd  41187  caratheodorylem1  41246  isomenndlem  41250  hoidmv1lelem2  41312  hoidmvlelem2  41316  hspmbllem2  41347  smflimsuplem1  41532  smflimsuplem4  41535  smflimsuplem7  41538  smflimsup  41540  funcrngcsetc  42508  funcrngcsetcALT  42509  funcringcsetc  42545  mgpsumunsn  42650  lmod1zr  42792
  Copyright terms: Public domain W3C validator