Theorem mpteq2dva 4255

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 1626	. 2 |- F/ x ph
2		mpteq2dva.1	. 2 |- ( ( ph /\ x e. A ) -> B = C )
3	1, 2	mpteq2da 4254	1 |- ( ph -> ( x e. A |-> B ) = ( x e. A |-> C ) )

Syntax hints:   -> wi 4   /\ wa 359   = wceq 1649   e. wcel 1721   e. cmpt 4226

This theorem is referenced by:  mpteq2dv  4256  offval  6271  offval2  6281  caofinvl  6290  caofcom  6295  caofass  6297  caofdi  6299  caofdir  6300  caonncan  6301  curry1  6397  curry2  6400  pw2f1olem  7171  mapxpen  7232  xpmapenlem  7233  cantnfp1  7593  cantnflem1d  7600  cantnflem1  7601  cnfcom2lem  7614  dfac12lem1  7979  seqof  11335  seqof2  11336  swrd0val  11723  revco  11758  ccatco  11759  lo1eq  12317  rlimeq  12318  lo1mul2  12377  o1dif  12378  lo1sub  12379  rlimdiv  12394  caucvgr  12424  fsumrlim  12545  fsumo1  12546  climfsum  12554  geomulcvg  12608  vdwlem8  13311  restid2  13613  pwsplusgval  13667  pwsmulrval  13668  pwsvscafval  13671  divsin  13724  xpsaddlem  13755  xpsvsca  13759  catidd  13860  fuclid  14118  fucrid  14119  fucass  14120  setcepi  14198  prf1st  14256  prf2nd  14257  1st2ndprf  14258  curfcl  14284  curfuncf  14290  diag2  14297  curf2ndf  14299  hof2val  14308  hofcllem  14310  hofcl  14311  yonedalem4a  14327  yonedalem4c  14329  yonedalem3b  14331  yonedainv  14333  yonffthlem  14334  prdsidlem  14682  prdsmndd  14683  pwsco2mhm  14725  frmdup3  14766  grpinvpropd  14821  prdsinvlem  14881  pwsinvg  14885  pwssub  14886  galactghm  15061  cayleylem1  15065  sylow1lem2  15188  sylow3lem1  15216  efginvrel1  15315  frgpup3lem  15364  frgpup3  15365  prdscmnd  15431  iscyggen  15445  gsumval3  15469  gsumcllem  15471  gsumzsplit  15484  gsumsub  15497  gsum2d  15501  gsum2d2  15503  gsumxp  15505  prdsgsum  15507  dprdfsub  15534  dprdfeq0  15535  dprddisj2  15552  dprd2d2  15557  dpjidcl  15571  ablfaclem2  15599  ablfac2  15602  gsumdixp  15670  prdsmgp  15671  prdsrngd  15673  prdslmodd  16000  asclpropd  16359  psrass1lem  16397  psrlinv  16416  psrass1  16424  psrdi  16425  psrdir  16426  psrcom  16427  psrass23  16428  resspsrmul  16435  mplsubrglem  16457  mplmonmul  16482  mplcoe1  16483  mplcoe2  16485  mplcoe4  16518  psrplusgpropd  16584  psropprmul  16587  coe1mul2  16617  coe1tm  16620  coe1tmmul2  16623  coe1tmmul  16624  coe1pwmul  16626  ply1coe  16639  mulgrhm2  16743  frgpcyg  16809  phlpropd  16841  neiptopnei  17151  neiptopreu  17152  ptcnplem  17606  cnmpt1t  17650  cnmpt12  17652  cnmptkp  17665  cnmptk1  17666  cnmpt1k  17667  cnmptkk  17668  cnmptk1p  17670  cnmpt2k  17673  qtopeu  17701  pt1hmeo  17791  ptunhmeo  17793  xkocnv  17799  xkohmeo  17800  flfcnp2  17992  cnmpt1plusg  18070  istgp2  18074  tmdmulg  18075  tgpmulg  18076  tmdgsum  18078  symgtgp  18084  subgtgp  18088  tgpconcomp  18095  prdstgpd  18107  tsmsmhm  18128  tsmsadd  18129  tsmssub  18131  tgptsmscls  18132  tsmssplit  18134  tsmsxplem1  18135  tsmsxplem2  18136  cnmpt1vsca  18176  tlmtgp  18178  ustuqtoplem  18222  utopsnneip  18231  ressprdsds  18354  metuvalOLD  18532  metuval  18533  nmfval2  18591  tngnm  18645  nmoeq0  18723  idnghm  18730  cnmpt1ds  18826  fsumcn  18853  expcn  18855  divccn  18856  divccncf  18889  negcncf  18901  copco  18996  pcopt  19000  pcopt2  19001  pcoass  19002  pi1xfrcnvlem  19034  cnmpt1ip  19154  minveclem3b  19282  ovolctb  19339  ovoliunnul  19356  voliunlem3  19399  ovolfs2  19416  uniioombllem2  19428  vitalilem4  19456  vitalilem5  19457  ismbf  19475  mbfss  19491  mbfmulc2re  19493  mbfneg  19495  mbfpos  19496  mbfposb  19498  mbfadd  19506  mbfsub  19507  mbfmulc2  19508  mbfinf  19510  mbflimsup  19511  mbflimlem  19512  i1fpos  19551  i1fposd  19552  itg1climres  19559  mbfmul  19571  itg2mulc  19592  itg2i1fseq  19600  itg2cnlem1  19606  itg2cnlem2  19607  itgresr  19623  iblneg  19647  i1fibl  19652  itgitg1  19653  iblsub  19666  itgfsum  19671  itgmulc2lem1  19676  limcmpt  19723  limccnp  19731  limcco  19733  dvreslem  19749  dvres2lem  19750  dvidlem  19755  dvcnp2  19759  dvaddbr  19777  dvmulbr  19778  dvmulf  19782  dvcmulf  19784  dvcobr  19785  dvcof  19787  dvcjbr  19788  dvcj  19789  dvfre  19790  dvexp  19792  dvexp2  19793  dvrec  19794  dvmptcmul  19803  dvmptdivc  19804  dvmptneg  19805  dvmptsub  19806  dvmptre  19808  dvmptim  19809  dvmptfsum  19812  dvcnvlem  19813  dvcnv  19814  dvexp3  19815  dvef  19817  dvsincos  19818  dv11cn  19838  lhop2  19852  lhop  19853  ftc2  19881  itgparts  19884  itgsubstlem  19885  evlslem3  19888  evlslem1  19889  mdegfval  19938  mdegmullem  19954  ply1termlem  20075  plypow  20077  plyconst  20078  plyeq0lem  20082  plypf1  20084  plyaddlem1  20085  plymullem1  20086  coeeulem  20096  coeidlem  20109  plyco  20113  coeeq2  20114  0dgr  20117  0dgrb  20118  dgrcolem1  20144  dgrcolem2  20145  plycjlem  20147  dvply1  20154  dvply2g  20155  plydiveu  20168  plyremlem  20174  elqaalem3  20191  taylfval  20228  dvtaylp  20239  taylthlem1  20242  taylthlem2  20243  ulmshft  20259  mtestbdd  20274  iblulm  20276  itgulm2  20278  pserulm  20291  psercn2  20292  pserdvlem2  20297  pserdv  20298  pserdv2  20299  abelthlem1  20300  abelthlem3  20302  advlog  20498  advlogexp  20499  dvcxp1  20579  dvcxp2  20580  sqrcn  20587  loglesqr  20595  dvatan  20728  atantayl2  20731  atantayl3  20732  leibpi  20735  rlimcnp2  20758  efrlim  20761  dfef2  20762  cxp2lim  20768  divsqrsumlem  20771  ftalem7  20814  basellem9  20824  muinv  20931  logfacrlim  20961  logexprlim  20962  dchrmulid2  20989  dchrinvcl  20990  lgseisenlem3  21088  lgseisenlem4  21089  chtppilimlem2  21121  chebbnd2  21124  chpchtlim  21126  chpo1ub  21127  rpvmasumlem  21134  dchrmusumlema  21140  dchrvmasumlem1  21142  dchrvmasumiflem2  21149  dchrisum0fno1  21158  rpvmasum2  21159  dchrisum0lema  21161  dchrisum0lem1  21163  dchrisum0lem2a  21164  dchrisum0lem2  21165  dchrisum0  21167  dchrmusumlem  21169  dchrvmasumlem  21170  rpvmasum  21173  rplogsum  21174  logdivsum  21180  mulog2sumlem3  21183  vmalogdivsum2  21185  vmalogdivsum  21186  2vmadivsumlem  21187  logsqvma2  21190  log2sumbnd  21191  selberglem2  21193  selberg3lem1  21204  selberg3  21206  selberg4lem1  21207  selberg4  21208  pntrsumo1  21212  selberg3r  21216  selberg4r  21217  selberg34r  21218  pntrlog2bndlem2  21225  pntrlog2bndlem4  21227  pntrlog2bndlem5  21228  pntrlog2bndlem6  21230  padicabvf  21278  padicabvcxp  21279  chscllem4  23095  brafnmul  23407  kbmul  23411  ofresid  24008  fmptapd  24014  ofoprabco  24032  gsumsn2  24172  xrge0mulc1cn  24280  esumval  24394  esumsn  24409  esumpcvgval  24421  esumcvg  24429  ofcfeqd2  24437  meascnbl  24526  sitgval  24600  probmeasb  24641  cndprobprob  24649  dstfrvclim1  24688  ballotlemfval  24700  ballotlemsval  24719  ballotlemieq  24727  lgamgulmlem2  24767  lgamgulm2  24773  lgamcvglem  24777  gamcvg2lem  24796  ptpcon  24873  cvmliftlem6  24930  cvmliftphtlem  24957  cvmlift3lem5  24963  divcnvlin  25165  ovoliunnfl  26147  voliunnfl  26149  volsupnfl  26150  mbfposadd  26153  itg2addnclem  26155  itg2addnclem3  26157  itg2addnc  26158  itgaddnclem2  26163  itgaddnc  26164  iblsubnc  26165  itgsubnc  26166  itgmulc2nclem1  26170  itgmulc2nclem2  26171  itgmulc2nc  26172  itgabsnc  26173  ftc1cnnclem  26177  areacirclem2  26181  areacirclem4  26183  areacirclem5  26185  areacirc  26187  upixp  26321  mzpsubst  26695  mzprename  26696  mzpcompact2lem  26698  eldioph2  26710  rabdiophlem2  26752  uvcresum  27110  frlmup1  27118  grpvrinv  27319  mhmvlin  27320  mamuass  27328  mamudi  27329  mamudir  27330  mamuvs1  27331  mamuvs2  27332  mendlmod  27369  mendassa  27370  expgrowthi  27418  expgrowth  27420  mulc1cncfg  27588  expcnfg  27593  clim1fr1  27594  ibliccsinexp  27612  itgsinexplem1  27615  itgsinexp  27616  stoweidlem4  27620  stirlinglem5  27694  swrdswrd  28011

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-ral 2671  df-opab 4227  df-mpt 4228