Theorem mpteq1d 5199

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

Step	Hyp	Ref	Expression
1		mpteq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		mpteq1 5198	. 2 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐵 ↦ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-opab 5172  df-mpt 5191

This theorem is used by:  csbmpt2  5541  mptimass  6073  fmptapd  7173  offval  7691  mposn  8104  offsplitfpar  8120  mpocurryd  8271  curf  8873  cantnff  9657  dfac12lem1  10150  ackbij2lem2  10245  swrd00  14716  swrdlend  14727  swrd0  14732  repswswrd  14859  repswrevw  14862  revco  14909  ccatco  14910  ofccat  15046  vdwapfval  17069  imasdsval  17607  mrcfval  17702  catidd  17774  curfpropd  18327  pwspjmhm  18945  grpinvfval  19108  grpinvfvalALT  19109  psgnfval  19633  psgnfvalfi  19646  odfval  19665  odfvalALT  19666  frgpup3lem  19910  gsum2d2  20107  gsumxp  20109  telgsumfzs  20122  dprd2d2  20179  srgbinom  20376  gsummgp0  20464  pwsco1rhm  20658  pwsco2rhm  20659  funcrngcsetc  20808  funcrngcsetcALT  20809  funcringcsetc  20842  staffval  21013  freshmansdream  21793  phlpropd  21874  pjfval  21925  asclfval  22099  asclpropd  22118  mpfrcl  22307  evlsval  22308  psdffval  22391  evls1rhmlem  22552  evl1fval  22559  mvmulfval  22770  submafval  22807  mdetfval  22814  nfimdetndef  22817  mdetfval1  22818  mdet0pr  22820  m1detdiag  22825  madufval  22865  minmar1fval  22874  gsummatr01  22887  pmatcollpw3fi1lem2  23018  pmatcollpw3fi1  23019  cpmadugsumlemF  23107  ispnrm  23570  ptval2  23833  ptpjcn  23843  xkoptsub  23886  kqval  23958  pt1hmeo  24038  fmval  24175  tmdgsum  24327  subgtgp  24337  prdstmdd  24356  prdsxmslem2  24761  nmfval  24820  lebnumlem1  25195  limcmpt2  26118  dvcmulf  26179  mdegfval  26294  ulmshft  26633  wwlksnextbij  30378  off2  33122  of0r  33160  mptiffisupp  33173  mptprop  33178  fmptunsnop  33180  gsummpt2co  33496  gsumhashmul  33515  gsummulsubdishift1  33516  gsumwrd2dccat  33526  elrgspnlem4  33693  elrspunidl  33864  evl1deg2  33995  ply1coedeg  34007  gsummoncoe1fz  34016  0mplrim  34032  splyval  34077  vietalem  34097  vieta  34098  algextdeglem4  34238  esumnul  34566  ofcfval4  34623  measdivcst  34743  omsfval  34813  signstfval  35080  signstf0  35084  signstfvn  35085  mrsubffval  36094  mrsubfval  36095  msubfval  36111  elmsubrn  36115  mvhfval  36120  msrfval  36124  fwddifval  36750  tailfval  36999  poimirlem24  38401  ftc1anc  38458  sdclem2  38500  erngfset  41680  erngfset-rN  41688  dvhfset  41961  dvhset  41962  zndvdchrrhm  42847  aks4d1p1p6  42947  aks6d1c1  42990  aks6d1c5lem3  43011  sticksstones11  43030  fsuppssindlem2  43446  fsuppssind  43447  mzpclval  43578  mzpcompact2  43605  fsovrfovd  44857  supcnvlimsupmpt  46577  cncfshiftioo  46728  cncfiooicc  46730  dvsinax  46749  iblspltprt  46809  itgspltprt  46815  itgiccshift  46816  dirkercncflem2  46940  fourierdlem90  47032  fourierdlem92  47034  sge0val  47202  sge0prle  47237  sge0ss  47248  sge0iunmptlemfi  47249  sge0p1  47250  sge0iunmptlemre  47251  sge0iunmpt  47254  sge0xp  47265  ismeannd  47303  caratheodorylem1  47362  isomenndlem  47366  hoidmv1lelem2  47428  hoidmvlelem2  47432  hspmbllem2  47463  smflimsuplem1  47656  smflimsuplem4  47659  smflimsuplem7  47662  smflimsup  47664  mgpsumunsn  49299  lmod1zr  49431  iinfssclem1  49988  dfswapf2  50195  swapfval  50196  swapf2vala  50204  swapf2f1o  50210  swapf2f1oaALT  50212  prcofpropd  50313  prcof2a  50323  prcof2  50324  lmdfval  50583  cmdfval  50584