Theorem mpteq2dva 4366

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

Hypothesis

Ref	Expression
mpteq2dva.1	|- ( ( ph /\ x e. A ) -> B = C )

Assertion

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

Distinct variable group:   ph, x

Allowed substitution hints:   A( x)   B( x)   C( x)

Proof of Theorem mpteq2dva

Step	Hyp	Ref	Expression
1		nfv 1672	. 2 |- F/ x ph
2		mpteq2dva.1	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	1, 2	mpteq2da 4365	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 369   = wceq 1362   e. wcel 1755   e. cmpt 4338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-ral 2710  df-opab 4339  df-mpt 4340

This theorem is referenced by:  mpteq2dv  4367  fmptapd  5889  offval  6316  offval2  6325  caofinvl  6336  caofcom  6341  caofass  6343  caofdi  6345  caofdir  6346  caonncan  6347  curry1  6653  curry2  6656  pw2f1olem  7403  mapxpen  7465  xpmapenlem  7466  cantnfp1  7877  cantnflem1d  7884  cantnflem1  7885  cantnfp1OLD  7903  cantnflem1dOLD  7907  cantnflem1OLD  7908  cnfcom2lem  7922  cnfcom2lemOLD  7930  dfac12lem1  8300  seqof  11847  seqof2  11848  swrd0val  12301  swrdswrd  12338  repswswrd  12406  repswrevw  12408  revco  12446  ccatco  12447  repsco  12451  lo1eq  13030  rlimeq  13031  lo1mul2  13090  o1dif  13091  lo1sub  13092  rlimdiv  13107  caucvgr  13137  sumeq1  13150  fsumrlim  13257  fsumo1  13258  climfsum  13266  geomulcvg  13319  vdwlem8  14032  restid2  14352  pwsplusgval  14411  pwsmulrval  14412  pwsvscafval  14415  divsin  14465  xpsaddlem  14496  xpsvsca  14500  catidd  14601  fuclid  14859  fucrid  14860  fucass  14861  setcepi  14939  prf1st  14997  prf2nd  14998  1st2ndprf  14999  curfcl  15025  curfuncf  15031  diag2  15038  curf2ndf  15040  hof2val  15049  hofcllem  15051  hofcl  15052  yonedalem4a  15068  yonedalem4c  15070  yonedalem3b  15072  yonedainv  15074  yonffthlem  15075  prdsidlem  15436  prdsmndd  15437  pwsco2mhm  15481  frmdup3  15524  grpinvpropd  15581  prdsinvlem  15643  pwsinvg  15647  pwssub  15648  galactghm  15888  cayleylem1  15897  pmtrprfval  15973  sylow1lem2  16078  sylow3lem1  16106  efginvrel1  16205  frgpup3lem  16254  frgpup3  16255  prdscmnd  16323  iscyggen  16337  gsumval3OLD  16362  gsumval3  16365  gsumcllem  16366  gsumcllemOLD  16367  gsumzsplit  16398  gsumzsplitOLD  16399  gsumsub  16423  gsumsubOLD  16424  gsumsnd  16426  gsum2d  16437  gsum2dOLD  16438  gsum2d2  16440  gsumxp  16442  gsumxpOLD  16444  prdsgsum  16445  prdsgsumOLD  16446  dprdfsub  16485  dprdfeq0  16486  dprdfsubOLD  16492  dprdfeq0OLD  16493  dprddisj2  16511  dprddisj2OLD  16512  dprd2d2  16517  dpjidcl  16531  dpjidclOLD  16538  ablfaclem2  16561  ablfac2  16564  gsumdixpOLD  16635  gsumdixp  16636  prdsmgp  16637  prdsrngd  16639  prdslmodd  16972  asclpropd  17338  psrass1lem  17381  psrlinv  17402  psrass1  17412  psrdi  17413  psrdir  17414  psrcom  17415  psrass23  17416  resspsrmul  17423  mplsubrglem  17451  mplsubrglemOLD  17452  mplmonmul  17477  mplcoe1  17478  mplcoe2  17481  mplcoe2OLD  17482  mplcoe4  17517  psrplusgpropd  17588  psropprmul  17591  coe1mul2  17621  coe1tm  17624  coe1tmmul2  17627  coe1tmmul  17628  coe1pwmul  17630  ply1coe  17643  mulgrhm2  17769  mulgrhm2OLD  17772  frgpcyg  17848  evpmodpmf1o  17868  phlpropd  17926  frlmphl  18048  uvcresum  18060  frlmup1  18068  mamures  18132  grpvrinv  18138  mhmvlin  18139  mamuass  18148  mamudi  18149  mamudir  18150  mamuvs1  18151  mamuvs2  18152  mamutpos  18185  madetsumid  18188  1mavmul  18201  mavmulass  18202  mvmumamul1  18207  mulmarep1gsum1  18226  mulmarep1gsum2  18227  mdetleib2  18241  mdetfval1  18243  mdet0pr  18245  mdet1  18250  mdetrlin  18251  mdetrsca  18252  mdetralt  18256  mdetunilem9  18268  gsummatr01  18307  smadiadetlem1a  18311  smadiadetlem3  18316  smadiadetlem4  18317  neiptopnei  18578  neiptopreu  18579  ptcnplem  19036  cnmpt1t  19080  cnmpt12  19082  cnmptkp  19095  cnmptk1  19096  cnmpt1k  19097  cnmptkk  19098  cnmptk1p  19100  cnmpt2k  19103  qtopeu  19131  pt1hmeo  19221  ptunhmeo  19223  xkocnv  19229  xkohmeo  19230  flfcnp2  19422  cnmpt1plusg  19500  istgp2  19504  tmdmulg  19505  tgpmulg  19506  tmdgsum  19508  symgtgp  19514  subgtgp  19518  tgpconcomp  19525  prdstgpd  19537  tsmsmhm  19562  tsmsadd  19563  tsmssub  19565  tgptsmscls  19566  tsmssplit  19568  tsmsxplem1  19569  tsmsxplem2  19570  cnmpt1vsca  19610  tlmtgp  19612  ustuqtoplem  19656  utopsnneip  19665  ressprdsds  19788  metuvalOLD  19966  metuval  19967  nmfval2  20025  tngnm  20079  nmoeq0  20157  idnghm  20164  cnmpt1ds  20261  fsumcn  20288  expcn  20290  divccn  20291  divccncf  20324  negcncf  20336  copco  20432  pcopt  20436  pcopt2  20437  pcoass  20438  pi1xfrcnvlem  20470  cnmpt1ip  20601  rrxnm  20737  rrxds  20739  minveclem3b  20757  ovolctb  20815  ovoliunnul  20832  voliunlem3  20875  ovolfs2  20893  uniioombllem2  20905  vitalilem4  20933  vitalilem5  20934  ismbf  20950  mbfss  20966  mbfmulc2re  20968  mbfneg  20970  mbfpos  20971  mbfposb  20973  mbfadd  20981  mbfsub  20982  mbfmulc2  20983  mbfinf  20985  mbflimsup  20986  mbflimlem  20987  i1fpos  21026  i1fposd  21027  itg1climres  21034  mbfmul  21046  itg2mulc  21067  itg2i1fseq  21075  itg2cnlem1  21081  itg2cnlem2  21082  itgresr  21098  iblneg  21122  i1fibl  21127  itgitg1  21128  iblsub  21141  itgfsum  21146  itgmulc2lem1  21151  limcmpt  21200  limccnp  21208  limcco  21210  dvreslem  21226  dvres2lem  21227  dvidlem  21232  dvcnp2  21236  dvaddbr  21254  dvmulbr  21255  dvmulf  21259  dvcmulf  21261  dvcobr  21262  dvcof  21264  dvcjbr  21265  dvcj  21266  dvfre  21267  dvexp  21269  dvexp2  21270  dvrec  21271  dvmptcmul  21280  dvmptdivc  21281  dvmptneg  21282  dvmptsub  21283  dvmptre  21285  dvmptim  21286  dvmptfsum  21289  dvcnvlem  21290  dvcnv  21291  dvexp3  21292  dvef  21294  dvsincos  21295  dv11cn  21315  lhop2  21329  lhop  21330  ftc2  21358  itgparts  21361  itgsubstlem  21362  evlslem3  21366  evlslem1  21367  mdegfval  21416  mdegmullem  21434  ply1termlem  21556  plypow  21558  plyconst  21559  plyeq0lem  21563  plypf1  21565  plyaddlem1  21566  plymullem1  21567  coeeulem  21577  coeidlem  21590  plyco  21594  coeeq2  21595  0dgr  21598  0dgrb  21599  dgrcolem1  21625  dgrcolem2  21626  plycjlem  21628  dvply1  21635  dvply2g  21636  plydiveu  21649  plyremlem  21655  elqaalem3  21672  taylfval  21709  dvtaylp  21720  taylthlem1  21723  taylthlem2  21724  ulmshft  21740  mtestbdd  21755  iblulm  21757  itgulm2  21759  pserulm  21772  psercn2  21773  pserdvlem2  21778  pserdv  21779  pserdv2  21780  abelthlem1  21781  abelthlem3  21783  advlog  21984  advlogexp  21985  dvcxp1  22065  dvcxp2  22066  sqrcn  22073  loglesqr  22081  dvatan  22215  atantayl2  22218  atantayl3  22219  leibpi  22222  rlimcnp2  22245  efrlim  22248  dfef2  22249  cxp2lim  22255  divsqrsumlem  22258  ftalem7  22301  basellem9  22311  muinv  22418  logfacrlim  22448  logexprlim  22449  dchrmulid2  22476  dchrinvcl  22477  lgseisenlem3  22575  lgseisenlem4  22576  chtppilimlem2  22608  chebbnd2  22611  chpchtlim  22613  chpo1ub  22614  rpvmasumlem  22621  dchrmusumlema  22627  dchrvmasumlem1  22629  dchrvmasumiflem2  22636  dchrisum0fno1  22645  rpvmasum2  22646  dchrisum0lema  22648  dchrisum0lem1  22650  dchrisum0lem2a  22651  dchrisum0lem2  22652  dchrisum0  22654  dchrmusumlem  22656  dchrvmasumlem  22657  rpvmasum  22660  rplogsum  22661  logdivsum  22667  mulog2sumlem3  22670  vmalogdivsum2  22672  vmalogdivsum  22673  2vmadivsumlem  22674  logsqvma2  22677  log2sumbnd  22678  selberglem2  22680  selberg3lem1  22691  selberg3  22693  selberg4lem1  22694  selberg4  22695  pntrsumo1  22699  selberg3r  22703  selberg4r  22704  selberg34r  22705  pntrlog2bndlem2  22712  pntrlog2bndlem4  22714  pntrlog2bndlem5  22715  pntrlog2bndlem6  22717  padicabvf  22765  padicabvcxp  22766  mirval  22925  chscllem4  24866  brafnmul  25178  kbmul  25182  ofresid  25784  ofoprabco  25806  fcobijfs  25850  gsumsn2  26092  gsummptf1o  26099  xrge0mulc1cn  26225  esumval  26354  esumsn  26369  esumpcvgval  26381  esumcvg  26389  ofcfeqd2  26397  meascnbl  26487  sitgval  26566  probmeasb  26661  cndprobprob  26669  dstfrvclim1  26708  ballotlemfval  26720  ballotlemsval  26739  ballotlemieq  26747  ofccat  26789  plymul02  26795  plymulx0  26796  plymulx  26797  signsplypnf  26799  signstfv  26812  signstfvn  26818  signstfvp  26820  lgamgulmlem2  26864  lgamgulm2  26870  lgamcvglem  26874  gamcvg2lem  26893  ptpcon  26970  cvmliftlem6  27027  cvmliftphtlem  27054  cvmlift3lem5  27060  divcnvlin  27246  ovoliunnfl  28277  voliunnfl  28279  volsupnfl  28280  mbfposadd  28283  itg2addnclem  28287  itg2addnclem3  28289  itg2addnc  28290  itgaddnclem2  28295  itgaddnc  28296  iblsubnc  28297  itgsubnc  28298  itgmulc2nclem1  28302  itgmulc2nclem2  28303  itgmulc2nc  28304  itgabsnc  28305  ftc1cnnclem  28309  ftc1anclem3  28313  ftc1anclem5  28315  ftc1anclem6  28316  ftc1anclem8  28318  ftc1anc  28319  ftc2nc  28320  dvcncxp1  28321  areacirclem1  28328  areacirclem2  28329  areacirclem4  28331  areacirc  28333  upixp  28467  mzpsubst  28930  mzprename  28931  mzpcompact2lem  28933  eldioph2  28945  rabdiophlem2  28985  mendlmod  29395  mendassa  29396  areaquad  29437  expgrowthi  29452  expgrowth  29454  mulc1cncfg  29616  expcnfg  29619  clim1fr1  29620  ibliccsinexp  29637  itgsinexplem1  29640  itgsinexp  29641  stoweidlem4  29645  stirlinglem5  29719  wwlknprop  30166  fdmdifeqresdif  30576  lincvalsc0  30664  linc0scn0  30666  lincdifsn  30667  lincsum  30672  lincscm  30673  lindslinindimp2lem4  30704  lindslinindsimp2lem5  30705  lincresunit3lem2  30723  bj-finsumval0  32159