MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq2dva Unicode version

Theorem mpteq2dva 4122
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
StepHypRef Expression
1 nfv 1609 . 2  |-  F/ x ph
2 mpteq2dva.1 . 2  |-  ( (
ph  /\  x  e.  A )  ->  B  =  C )
31, 2mpteq2da 4121 1  |-  ( ph  ->  ( x  e.  A  |->  B )  =  ( x  e.  A  |->  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632    e. wcel 1696    e. cmpt 4093
This theorem is referenced by:  mpteq2dv  4123  offval  6101  offval2  6111  caofinvl  6120  caofcom  6125  caofass  6127  caofdi  6129  caofdir  6130  caonncan  6131  curry1  6226  curry2  6229  pw2f1olem  6982  mapxpen  7043  xpmapenlem  7044  cantnfp1  7399  cantnflem1d  7406  cantnflem1  7407  cnfcom2lem  7420  dfac12lem1  7785  seqof  11119  swrd0val  11470  revco  11505  ccatco  11506  lo1eq  12058  rlimeq  12059  lo1mul2  12118  o1dif  12119  lo1sub  12120  rlimdiv  12135  caucvgr  12164  fsumrlim  12285  fsumo1  12286  climfsum  12294  geomulcvg  12348  vdwlem8  13051  restid2  13351  pwsplusgval  13405  pwsmulrval  13406  pwsvscafval  13409  divsin  13462  xpsaddlem  13493  xpsvsca  13497  catidd  13598  cidpropd  13629  monpropd  13656  fuclid  13856  fucrid  13857  fucass  13858  setcepi  13936  prf1st  13994  prf2nd  13995  1st2ndprf  13996  curfcl  14022  curfuncf  14028  diag2  14035  curf2ndf  14037  hof2val  14046  hofcllem  14048  hofcl  14049  yonedalem4a  14065  yonedalem4c  14067  yonedalem3b  14069  yonedainv  14071  yonffthlem  14072  prdsidlem  14420  prdsmndd  14421  pwsco2mhm  14463  frmdup3  14504  grpinvpropd  14559  prdsinvlem  14619  pwsinvg  14623  pwssub  14624  galactghm  14799  cayleylem1  14803  sylow1lem2  14926  sylow3lem1  14954  efginvrel1  15053  frgpup3lem  15102  frgpup3  15103  prdscmnd  15169  iscyggen  15183  gsumval3  15207  gsumcllem  15209  gsumzsplit  15222  gsumsub  15235  gsum2d  15239  gsum2d2  15241  gsumxp  15243  prdsgsum  15245  dprdfsub  15272  dprdfeq0  15273  dprddisj2  15290  dprd2d2  15295  dpjidcl  15309  ablfaclem2  15337  ablfac2  15340  gsumdixp  15408  prdsmgp  15409  prdsrngd  15411  prdslmodd  15742  asclpropd  16101  psrass1lem  16139  psrlinv  16158  psrass1  16166  psrdi  16167  psrdir  16168  psrcom  16169  psrass23  16170  resspsrmul  16177  mplsubrglem  16199  mplmonmul  16224  mplcoe1  16225  mplcoe2  16227  mplcoe4  16260  psrplusgpropd  16329  psropprmul  16332  coe1mul2  16362  coe1tm  16365  coe1tmmul2  16368  coe1tmmul  16369  coe1pwmul  16371  ply1coe  16384  mulgrhm2  16477  frgpcyg  16543  phlpropd  16575  ptcnplem  17331  cnmpt1t  17375  cnmpt12  17377  cnmptkp  17390  cnmptk1  17391  cnmpt1k  17392  cnmptkk  17393  cnmptk1p  17395  cnmpt2k  17398  qtopeu  17423  pt1hmeo  17513  ptunhmeo  17515  xkocnv  17521  xkohmeo  17522  flfcnp2  17718  cnmpt1plusg  17786  istgp2  17790  tmdmulg  17791  tgpmulg  17792  tmdgsum  17794  symgtgp  17800  subgtgp  17804  tgpconcomp  17811  prdstgpd  17823  tsmsmhm  17844  tsmsadd  17845  tsmssub  17847  tgptsmscls  17848  tsmssplit  17850  tsmsxplem1  17851  tsmsxplem2  17852  cnmpt1vsca  17892  tlmtgp  17894  ressprdsds  17951  nmfval2  18129  tngnm  18183  nmoeq0  18261  idnghm  18268  cnmpt1ds  18363  fsumcn  18390  expcn  18392  divccn  18393  divccncf  18426  negcncf  18437  copco  18532  pcopt  18536  pcopt2  18537  pcoass  18538  pi1xfrcnvlem  18570  cnmpt1ip  18690  minveclem3b  18808  ovolctb  18865  ovoliunnul  18882  voliunlem3  18925  ovolfs2  18942  uniioombllem2  18954  vitalilem4  18982  vitalilem5  18983  ismbf  19001  mbfss  19017  mbfmulc2re  19019  mbfneg  19021  mbfpos  19022  mbfposb  19024  mbfadd  19032  mbfsub  19033  mbfmulc2  19034  mbfinf  19036  mbflimsup  19037  mbflimlem  19038  i1fpos  19077  i1fposd  19078  itg1climres  19085  mbfmul  19097  itg2mulc  19118  itg2i1fseq  19126  itg2cnlem1  19132  itg2cnlem2  19133  itgresr  19149  iblneg  19173  i1fibl  19178  itgitg1  19179  iblsub  19192  itgfsum  19197  itgmulc2lem1  19202  limcmpt  19249  limccnp  19257  limcco  19259  dvreslem  19275  dvres2lem  19276  dvidlem  19281  dvcnp2  19285  dvaddbr  19303  dvmulbr  19304  dvmulf  19308  dvcmulf  19310  dvcobr  19311  dvcof  19313  dvcjbr  19314  dvcj  19315  dvfre  19316  dvexp  19318  dvexp2  19319  dvrec  19320  dvmptcmul  19329  dvmptdivc  19330  dvmptneg  19331  dvmptsub  19332  dvmptre  19334  dvmptim  19335  dvmptfsum  19338  dvcnvlem  19339  dvcnv  19340  dvexp3  19341  dvef  19343  dvsincos  19344  dv11cn  19364  lhop2  19378  lhop  19379  ftc2  19407  itgparts  19410  itgsubstlem  19411  evlslem3  19414  evlslem1  19415  mdegfval  19464  mdegmullem  19480  ply1termlem  19601  plypow  19603  plyconst  19604  plyeq0lem  19608  plypf1  19610  plyaddlem1  19611  plymullem1  19612  coeeulem  19622  coeidlem  19635  plyco  19639  coeeq2  19640  0dgr  19643  0dgrb  19644  dgrcolem1  19670  dgrcolem2  19671  plycjlem  19673  dvply1  19680  dvply2g  19681  plydiveu  19694  plyremlem  19700  elqaalem3  19717  taylfval  19754  dvtaylp  19765  taylthlem1  19768  taylthlem2  19769  ulmshft  19785  iblulm  19799  itgulm2  19801  pserulm  19814  psercn2  19815  pserdvlem2  19820  pserdv  19821  pserdv2  19822  abelthlem1  19823  abelthlem3  19825  advlog  20017  advlogexp  20018  dvcxp1  20098  dvcxp2  20099  sqrcn  20106  loglesqr  20114  dvatan  20247  atantayl2  20250  atantayl3  20251  leibpi  20254  rlimcnp2  20277  efrlim  20280  dfef2  20281  cxp2lim  20287  divsqrsumlem  20290  ftalem7  20332  basellem9  20342  muinv  20449  logfacrlim  20479  logexprlim  20480  dchrmulid2  20507  dchrinvcl  20508  lgseisenlem3  20606  lgseisenlem4  20607  chtppilimlem2  20639  chebbnd2  20642  chpchtlim  20644  chpo1ub  20645  rpvmasumlem  20652  dchrmusumlema  20658  dchrvmasumlem1  20660  dchrvmasumiflem2  20667  dchrisum0fno1  20676  rpvmasum2  20677  dchrisum0lema  20679  dchrisum0lem1  20681  dchrisum0lem2a  20682  dchrisum0lem2  20683  dchrisum0  20685  dchrmusumlem  20687  dchrvmasumlem  20688  rpvmasum  20691  rplogsum  20692  logdivsum  20698  mulog2sumlem3  20701  vmalogdivsum2  20703  vmalogdivsum  20704  2vmadivsumlem  20705  logsqvma2  20708  log2sumbnd  20709  selberglem2  20711  selberg3lem1  20722  selberg3  20724  selberg4lem1  20725  selberg4  20726  pntrsumo1  20730  selberg3r  20734  selberg4r  20735  selberg34r  20736  pntrlog2bndlem2  20743  pntrlog2bndlem4  20745  pntrlog2bndlem5  20746  pntrlog2bndlem6  20748  padicabvf  20796  padicabvcxp  20797  chscllem4  22235  brafnmul  22547  kbmul  22551  ballotlemfval  23064  ballotlemsval  23083  ballotlemieq  23091  fmptapd  23228  ofoprabco  23247  gsumsn2  23393  esumval  23440  esumsn  23452  esumpcvgval  23461  esumcvg  23469  ofcfeqd2  23477  meascnbl  23561  probmeasb  23648  dstfrvclim1  23693  ptpcon  23779  cvmliftlem6  23836  cvmliftphtlem  23863  cvmlift3lem5  23869  ovoliunnfl  25001  itg2addnclem  25003  itg2addnc  25005  itgaddnclem2  25010  itgaddnc  25011  iblsubnc  25012  itgsubnc  25013  itgmulc2nclem1  25017  itgmulc2nclem2  25018  itgmulc2nc  25019  itgabsnc  25020  ftc1cnnclem  25024  areacirclem2  25028  areacirclem4  25030  areacirclem5  25032  areacirc  25034  curgrpact  25475  cmprtr  25499  cmpltr2  25510  cmperltr  25512  cmprltr  25513  addcomv  25758  addassv  25759  addidv2  25760  cnegvex2  25763  rnegvex2  25764  issubrv  25775  mulone  25788  mulmulvec  25790  distmlva  25791  distsava  25792  upixp  26506  mzpsubst  26929  mzprename  26930  mzpcompact2lem  26932  eldioph2  26944  rabdiophlem2  26986  uvcresum  27345  frlmup1  27353  grpvrinv  27554  mhmvlin  27555  mamuass  27563  mamudi  27564  mamudir  27565  mamuvs1  27566  mamuvs2  27567  mendlmod  27604  mendassa  27605  expgrowthi  27653  expgrowth  27655  mulc1cncfg  27824  expcnfg  27829  clim1fr1  27830  ibliccsinexp  27848  itgsinexplem1  27851  itgsinexp  27852  stirlinglem5  27930
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-ral 2561  df-opab 4094  df-mpt 4095
  Copyright terms: Public domain W3C validator