Theorem mpteq2dva 4672

Description: Slightly more general equality inference for the maps to notation. (Contributed by Scott Fenton, 25-Apr-2012.)

Hypothesis

Ref	Expression
mpteq2dva.1	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2dva	⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Distinct variable group:   𝜑,𝑥

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		nfv 1830	. 2 ⊢ Ⅎ𝑥𝜑
2		mpteq2dva.1	. 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	1, 2	mpteq2da 4671	1 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ↦ cmpt 4643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-ral 2901  df-opab 4644  df-mpt 4645

This theorem is referenced by:  mpteq2dv  4673  2fvcoidd  6452  offval  6802  offval2  6812  caofinvl  6822  caofcom  6827  caofass  6829  caofdi  6831  caofdir  6832  caonncan  6833  curry1  7156  curry2  7159  mpt2curryd  7282  pw2f1olem  7949  mapxpen  8011  xpmapenlem  8012  cantnfp1  8461  cantnflem1d  8468  cantnflem1  8469  cnfcom2lem  8481  dfac12lem1  8848  seqof  12720  seqof2  12721  swrd0val  13273  swrdswrd  13312  repswswrd  13382  repswrevw  13384  revco  13431  ccatco  13432  repsco  13436  ofccat  13556  lo1eq  14147  rlimeq  14148  lo1mul2  14207  o1dif  14208  lo1sub  14209  rlimdiv  14224  caucvgr  14254  sumeq1  14267  fsumrlim  14384  fsumo1  14385  climfsum  14393  geomulcvg  14446  vdwlem8  15530  prmgapprmo  15604  restid2  15914  pwsplusgval  15973  pwsmulrval  15974  pwsvscafval  15977  qusin  16027  xpsaddlem  16058  xpsvsca  16062  catidd  16164  fuclid  16449  fucrid  16450  fucass  16451  setcepi  16561  prf1st  16667  prf2nd  16668  1st2ndprf  16669  curfcl  16695  curfuncf  16701  diag2  16708  curf2ndf  16710  hof2val  16719  hofcllem  16721  hofcl  16722  yonedalem4a  16738  yonedalem4c  16740  yonedalem3b  16742  yonedainv  16744  yonffthlem  16745  prdsidlem  17145  prdsmndd  17146  pwsco2mhm  17194  frmdup3lem  17226  frmdup3  17227  grpinvpropd  17313  prdsinvlem  17347  pwsinvg  17351  pwssub  17352  galactghm  17646  cayleylem1  17655  pmtrprfval  17730  sylow1lem2  17837  sylow3lem1  17865  efginvrel1  17964  frgpup3lem  18013  frgpup3  18014  prdscmnd  18087  iscyggen  18105  gsumval3  18131  gsumcllem  18132  gsumzsplit  18150  gsumsub  18171  gsummptf1o  18185  gsum2d  18194  gsum2d2  18196  gsumxp  18198  prdsgsum  18200  telgsumfz  18210  telgsumfz0  18212  telgsum  18214  dprdfsub  18243  dprdfeq0  18244  dprddisj2  18261  dprd2d2  18266  dpjidcl  18280  ablfaclem2  18308  ablfac2  18311  srgbinomlem3  18365  srgbinomlem4  18366  srgbinomlem  18367  gsumdixp  18432  prdsmgp  18433  prdsringd  18435  prdslmodd  18790  asclpropd  19167  psrass1lem  19198  psrlinv  19218  psrass1  19226  psrdi  19227  psrdir  19228  psrass23l  19229  psrcom  19230  psrass23  19231  resspsrmul  19238  mplsubrglem  19260  mplmonmul  19285  mplcoe1  19286  mplcoe5  19289  mplcoe4  19324  evlslem3  19335  evlslem1  19336  psrplusgpropd  19427  psropprmul  19429  coe1mul2  19460  coe1tm  19464  coe1tmmul2  19467  coe1tmmul  19468  coe1pwmul  19470  cply1mul  19485  ply1coe  19487  eqcoe1ply1eq  19488  lply1binomsc  19498  evl1gsummon  19550  mulgrhm2  19666  frgpcyg  19741  evpmodpmf1o  19761  phlpropd  19819  frlmphl  19939  uvcresum  19951  frlmup1  19956  mamures  20015  grpvrinv  20021  mhmvlin  20022  mamuass  20027  mamudi  20028  mamudir  20029  mamuvs1  20030  mamuvs2  20031  mpt2matmul  20071  mamutpos  20083  madetsumid  20086  dmatmul  20122  scmatscm  20138  1mavmul  20173  mavmulass  20174  mvmumamul1  20179  mulmarep1gsum1  20198  mulmarep1gsum2  20199  mdetleib2  20213  mdetfval1  20215  mdet0pr  20217  mdetdiag  20224  mdetdiagid  20225  mdetrlin  20227  mdetrsca  20228  mdetralt  20233  mdetunilem9  20245  gsummatr01  20284  smadiadetlem1a  20288  smadiadetlem3  20293  smadiadetlem4  20294  cpmatmcllem  20342  mat2pmatmul  20355  decpmatmullem  20395  decpmatmul  20396  pmatcollpw1lem2  20399  pmatcollpw  20405  pmatcollpw3lem  20407  pmatcollpwscmat  20415  idpm2idmp  20425  mp2pm2mplem3  20432  mp2pm2mplem4  20433  mp2pm2mplem5  20434  mp2pm2mp  20435  pm2mpghm  20440  pm2mpmhmlem2  20443  monmat2matmon  20448  pm2mp  20449  chpdmat  20465  chpscmat  20466  chpscmatgsumbin  20468  chpscmatgsummon  20469  chp0mat  20470  chpidmat  20471  chfacfscmulgsum  20484  chfacfpmmulgsum  20488  chfacfpmmulgsum2  20489  cayhamlem1  20490  cpmidgsumm2pm  20493  cpmidpmat  20497  cpmadugsumlemB  20498  cpmadugsumlemC  20499  cpmadugsumlemF  20500  cpmadumatpoly  20507  cayhamlem3  20511  cayhamlem4  20512  cayleyhamilton0  20513  cayleyhamiltonALT  20515  neiptopnei  20746  neiptopreu  20747  ptcnplem  21234  cnmpt1t  21278  cnmpt12  21280  cnmptkp  21293  cnmptk1  21294  cnmpt1k  21295  cnmptkk  21296  cnmptk1p  21298  cnmpt2k  21301  qtopeu  21329  pt1hmeo  21419  ptunhmeo  21421  xkocnv  21427  xkohmeo  21428  flfcnp2  21621  cnmpt1plusg  21701  istgp2  21705  tmdmulg  21706  tgpmulg  21707  tmdgsum  21709  symgtgp  21715  subgtgp  21719  tgpconcomp  21726  prdstgpd  21738  tsmsmhm  21759  tsmsadd  21760  tsmssub  21762  tgptsmscls  21763  tsmssplit  21765  tsmsxplem1  21766  tsmsxplem2  21767  cnmpt1vsca  21807  tlmtgp  21809  ustuqtoplem  21853  utopsnneip  21862  ressprdsds  21986  metuval  22164  nmfval2  22205  tngnm  22265  nmoeq0  22350  idnghm  22357  cnmpt1ds  22453  fsumcn  22481  expcn  22483  divccn  22484  divccncf  22517  negcncf  22529  copco  22626  pcopt  22630  pcopt2  22631  pcoass  22632  pi1xfrcnvlem  22664  cnmpt1ip  22854  rrxnm  22987  rrxds  22989  minveclem3b  23007  ovolctb  23065  ovoliunnul  23082  voliunlem3  23127  ovolfs2  23145  uniioombllem2  23157  vitalilem4  23186  vitalilem5  23187  ismbf  23203  mbfss  23219  mbfmulc2re  23221  mbfneg  23223  mbfpos  23224  mbfposb  23226  mbfadd  23234  mbfsub  23235  mbfmulc2  23236  mbfinf  23238  mbflimsup  23239  mbflimlem  23240  i1fpos  23279  i1fposd  23280  itg1climres  23287  mbfmul  23299  itg2mulc  23320  itg2i1fseq  23328  itg2cnlem1  23334  itg2cnlem2  23335  itgresr  23351  iblneg  23375  i1fibl  23380  itgitg1  23381  iblsub  23394  itgfsum  23399  itgmulc2lem1  23404  limcmpt  23453  limccnp  23461  limcco  23463  dvreslem  23479  dvres2lem  23480  dvidlem  23485  dvcnp2  23489  dvaddbr  23507  dvmulbr  23508  dvmulf  23512  dvcmulf  23514  dvcobr  23515  dvcof  23517  dvcjbr  23518  dvcj  23519  dvfre  23520  dvexp  23522  dvexp2  23523  dvrec  23524  dvmptcmul  23533  dvmptdivc  23534  dvmptneg  23535  dvmptsub  23536  dvmptre  23538  dvmptim  23539  dvmptfsum  23542  dvcnvlem  23543  dvcnv  23544  dvexp3  23545  dvef  23547  dvsincos  23548  dv11cn  23568  lhop2  23582  lhop  23583  ftc2  23611  itgparts  23614  itgsubstlem  23615  mdegfval  23626  mdegmullem  23642  ply1termlem  23763  plypow  23765  plyconst  23766  plyeq0lem  23770  plypf1  23772  plyaddlem1  23773  plymullem1  23774  coeeulem  23784  coeidlem  23797  plyco  23801  coeeq2  23802  0dgr  23805  0dgrb  23806  dgrcolem1  23833  dgrcolem2  23834  plycjlem  23836  dvply1  23843  dvply2g  23844  plydiveu  23857  plyremlem  23863  elqaalem3  23880  taylfval  23917  dvtaylp  23928  taylthlem1  23931  taylthlem2  23932  ulmshft  23948  mtestbdd  23963  iblulm  23965  itgulm2  23967  pserulm  23980  psercn2  23981  pserdvlem2  23986  pserdv  23987  pserdv2  23988  abelthlem1  23989  abelthlem3  23991  advlog  24200  advlogexp  24201  dvcxp1  24281  dvcxp2  24282  dvcncxp1  24284  sqrtcn  24291  loglesqrt  24299  dvatan  24462  atantayl2  24465  atantayl3  24466  leibpi  24469  rlimcnp2  24493  efrlim  24496  dfef2  24497  cxp2lim  24503  divsqrtsumlem  24506  lgamgulmlem2  24556  lgamgulm2  24562  lgamcvglem  24566  gamcvg2lem  24585  ftalem7  24605  basellem9  24615  muinv  24719  logfacrlim  24749  logexprlim  24750  dchrmulid2  24777  dchrinvcl  24778  lgseisenlem3  24902  lgseisenlem4  24903  chtppilimlem2  24963  chebbnd2  24966  chpchtlim  24968  chpo1ub  24969  rpvmasumlem  24976  dchrmusumlema  24982  dchrvmasumlem1  24984  dchrvmasumiflem2  24991  dchrisum0fno1  25000  rpvmasum2  25001  dchrisum0lema  25003  dchrisum0lem1  25005  dchrisum0lem2a  25006  dchrisum0lem2  25007  dchrisum0  25009  dchrmusumlem  25011  dchrvmasumlem  25012  rpvmasum  25015  rplogsum  25016  logdivsum  25022  mulog2sumlem3  25025  vmalogdivsum2  25027  vmalogdivsum  25028  2vmadivsumlem  25029  logsqvma2  25032  log2sumbnd  25033  selberglem2  25035  selberg3lem1  25046  selberg3  25048  selberg4lem1  25049  selberg4  25050  pntrsumo1  25054  selberg3r  25058  selberg4r  25059  selberg34r  25060  pntrlog2bndlem2  25067  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntrlog2bndlem6  25072  padicabvf  25120  padicabvcxp  25121  mirval  25350  wwlknprop  26214  chscllem4  27883  brafnmul  28194  kbmul  28198  ofresid  28824  ofoprabco  28847  fcobijfs  28889  gsummpt2d  29112  gsummptres  29115  fzto1st1  29183  fzto1st  29184  mdetpmtr1  29217  mdetlap  29226  xrge0mulc1cn  29315  esumval  29435  esumsnf  29453  esumpcvgval  29467  esumcvg  29475  esumcvgsum  29477  esumsup  29478  ofcfeqd2  29490  meascnbl  29609  sitgval  29721  probmeasb  29819  cndprobprob  29827  dstfrvclim1  29866  ballotlemfval  29878  ballotlemsval  29897  ballotlemieq  29905  plymul02  29949  plymulx0  29950  plymulx  29951  signsplypnf  29953  signstfv  29966  signstfvn  29972  signstfvp  29974  ptpcon  30469  cvmliftlem6  30526  cvmliftphtlem  30553  cvmlift3lem5  30559  elmrsubrn  30671  msubfval  30675  msubco  30682  divcnvlin  30871  knoppcnlem9  31661  knoppcnlem10  31662  knoppcnlem11  31663  bj-finsumval0  32324  curf  32557  matunitlindflem1  32575  matunitlindflem2  32576  poimirlem3  32582  poimirlem15  32594  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  broucube  32613  ovoliunnfl  32621  voliunnfl  32623  volsupnfl  32624  mbfposadd  32627  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  itgaddnclem2  32639  itgaddnc  32640  iblsubnc  32641  itgsubnc  32642  itgmulc2nclem1  32646  itgmulc2nclem2  32647  itgmulc2nc  32648  itgabsnc  32649  ftc1cnnclem  32653  ftc1anclem3  32657  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem8  32662  ftc1anc  32663  ftc2nc  32664  areacirclem1  32670  areacirclem2  32671  areacirclem4  32673  areacirc  32675  upixp  32694  mzpsubst  36329  mzprename  36330  mzpcompact2lem  36332  eldioph2  36343  rabdiophlem2  36384  mendlmod  36782  mendassa  36783  areaquad  36821  fsovcnvlem  37327  hashnzfzclim  37543  expgrowthi  37554  expgrowth  37556  uzmptshftfval  37567  dvradcnv2  37568  binomcxplemrat  37571  binomcxplemfrat  37572  binomcxplemradcnv  37573  binomcxplemdvbinom  37574  binomcxplemcvg  37575  binomcxplemdvsum  37576  binomcxplemnotnn0  37577  mulc1cncfg  38656  expcnfg  38658  fprodcnlem  38666  clim1fr1  38668  divcnvg  38694  sublimc  38719  reclimc  38720  divlimc  38723  cncfmptssg  38755  negcncfg  38766  divcncf  38769  cncficcgt0  38774  fprodcncf  38787  fprodsubrecnncnvlem  38794  fprodaddrecnncnvlem  38796  dvrecg  38800  dvsinax  38801  dvmptdiv  38807  dvasinbx  38810  dvdivf  38812  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnmptdivc  38828  dvxpaek  38830  dvnxpaek  38832  dvnmul  38833  dvnprodlem2  38837  ibliccsinexp  38842  itgsinexplem1  38845  itgsinexp  38846  iblempty  38857  itgcoscmulx  38861  itgsincmulx  38866  itgioocnicc  38869  iblcncfioo  38870  itgsbtaddcnst  38874  volioofmpt  38887  volicofmpt  38890  stoweidlem4  38897  stirlinglem5  38971  dirkerval  38984  dirkertrigeq  38994  dirkeritg  38995  dirkercncflem2  38997  dirkercncflem4  38999  fourierdlem16  39016  fourierdlem18  39018  fourierdlem21  39021  fourierdlem22  39022  fourierdlem28  39028  fourierdlem39  39039  fourierdlem40  39040  fourierdlem41  39041  fourierdlem53  39052  fourierdlem56  39055  fourierdlem57  39056  fourierdlem60  39059  fourierdlem61  39060  fourierdlem68  39067  fourierdlem73  39072  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem78  39077  fourierdlem81  39080  fourierdlem82  39081  fourierdlem83  39082  fourierdlem84  39083  fourierdlem85  39084  fourierdlem88  39087  fourierdlem90  39089  fourierdlem92  39091  fourierdlem93  39092  fourierdlem95  39094  fourierdlem97  39096  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  fourierdlem112  39111  sqwvfoura  39121  sqwvfourb  39122  fouriersw  39124  elaa2lem  39126  etransclem4  39131  etransclem17  39144  etransclem18  39145  etransclem32  39159  etransclem46  39173  sge0z  39268  sge0revalmpt  39271  sge0tsms  39273  sge0sup  39284  sge0iunmptlemre  39308  sge0iun  39312  sge0xaddlem2  39327  ismeannd  39360  psmeasurelem  39363  meaiuninclem  39373  meaiininclem  39376  caratheodory  39418  isomenndlem  39420  ovnval  39431  hoicvrrex  39446  ovnlecvr  39448  ovncvrrp  39454  ovn0lem  39455  ovnsubaddlem1  39460  hoidmv1lelem2  39482  hoidmv1le  39484  hoidmvlelem3  39487  ovnhoilem2  39492  ovnhoi  39493  ovnlecvr2  39500  ovncvr2  39501  hspmbllem2  39517  ovolval2lem  39533  ovolval3  39537  ovolval5lem1  39542  ovolval5lem2  39543  ovnovollem1  39546  ovnovollem2  39547  vonioolem1  39571  vonicclem1  39574  vonct  39584  smflim  39663  crctcshlem4  41023  eucrct2eupth  41413  fdmdifeqresdif  41913  ply1mulgsumlem2  41969  lincvalsc0  42004  linc0scn0  42006  lincdifsn  42007  lincsum  42012  lincscm  42013  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  lincresunit3lem2  42063  aacllem  42356  amgmwlem  42357