Theorem mpteq1d 4738

Description: An equality theorem for the maps to notation. (Contributed by Mario Carneiro, 11-Jun-2016.)

Hypothesis

Ref	Expression
mpteq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
mpteq1d	|- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )

Distinct variable groups:   x, A   x, B

Allowed substitution hints:   ph( x)   C( x)

Proof of Theorem mpteq1d

Step	Hyp	Ref	Expression
1		mpteq1d.1	. 2 |- ( ph -> A = B )
2		mpteq1 4737	. 2 |- ( A = B -> ( x e. A |-> C ) = ( x e. B |-> C ) )
3	1, 2	syl 17	1 |- ( ph -> ( x e. A |-> C ) = ( x e. B |-> C ) )

Syntax hints:   -> wi 4   = wceq 1483   |-> cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  csbmpt2  5011  fmptapd  6437  offval  6904  mpt2sn  7268  mpt2curryd  7395  cantnff  8571  dfac12lem1  8965  ackbij2lem2  9062  swrd00  13418  swrd0val  13421  swrdlend  13431  swrd0  13434  repswswrd  13531  repswrevw  13533  revco  13580  ccatco  13581  ofccat  13708  vdwapfval  15675  imasdsval  16175  mrcfval  16268  catidd  16341  curfpropd  16873  pwspjmhm  17368  grpinvfval  17460  psgnfval  17920  psgnfvalfi  17933  odfval  17952  frgpup3lem  18190  gsum2d2  18373  gsumxp  18375  telgsumfzs  18386  dprd2d2  18443  srgbinom  18545  gsummgp0  18608  pwsco1rhm  18738  pwsco2rhm  18739  staffval  18847  asclfval  19334  asclpropd  19346  mpfrcl  19518  evlsval  19519  evls1rhmlem  19686  evl1fval  19692  phlpropd  20000  pjfval  20050  mvmulfval  20348  submafval  20385  mdetfval  20392  nfimdetndef  20395  mdetfval1  20396  mdet0pr  20398  m1detdiag  20403  madufval  20443  minmar1fval  20452  gsummatr01  20465  pmatcollpw3fi1lem2  20592  pmatcollpw3fi1  20593  cpmadugsumlemF  20681  ispnrm  21143  ptval2  21404  ptpjcn  21414  xkoptsub  21457  kqval  21529  pt1hmeo  21609  fmval  21747  tmdgsum  21899  subgtgp  21909  prdstmdd  21927  prdsxmslem2  22334  nmfval  22393  lebnumlem1  22760  limcmpt2  23648  dvcmulf  23708  mdegfval  23822  ulmshft  24144  wwlksnextbij  26797  off2  29443  gsummpt2co  29780  esumnul  30110  ofcfval4  30167  measdivcst  30288  omsfval  30356  signstfval  30641  signstf0  30645  signstfvn  30646  mrsubffval  31404  mrsubfval  31405  msubfval  31421  elmsubrn  31425  mvhfval  31430  msrfval  31434  fwddifval  32269  tailfval  32367  curf  33387  poimirlem24  33433  ftc1anc  33493  sdclem2  33538  erngfset  36087  erngfset-rN  36095  dvhfset  36369  dvhset  36370  mzpclval  37288  mzpcompact2  37315  fsovrfovd  38303  mptima2  39457  supcnvlimsupmpt  39973  cncfshiftioo  40105  cncfiooicc  40107  dvsinax  40127  iblspltprt  40189  itgspltprt  40195  itgiccshift  40196  dirkercncflem2  40321  fourierdlem90  40413  fourierdlem92  40415  sge0val  40583  sge0prle  40618  sge0ss  40629  sge0iunmptlemfi  40630  sge0p1  40631  sge0iunmptlemre  40632  sge0iunmpt  40635  sge0xp  40646  ismeannd  40684  caratheodorylem1  40740  isomenndlem  40744  hoidmv1lelem2  40806  hoidmvlelem2  40810  hspmbllem2  40841  smflimsuplem1  41026  smflimsuplem4  41029  smflimsuplem7  41032  smflimsup  41034  funcrngcsetc  41998  funcrngcsetcALT  41999  funcringcsetc  42035  mgpsumunsn  42140  lmod1zr  42282