MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpteq2dv Structured version   Visualization version   GIF version

Theorem mpteq2dv 5206
Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 23-Aug-2014.)
Hypothesis
Ref Expression
mpteq2dv.1 (𝜑𝐵 = 𝐶)
Assertion
Ref Expression
mpteq2dv (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐶(𝑥)

Proof of Theorem mpteq2dv
StepHypRef Expression
1 mpteq2dv.1 . . 3 (𝜑𝐵 = 𝐶)
21adantr 482 . 2 ((𝜑𝑥𝐴) → 𝐵 = 𝐶)
32mpteq2dva 5204 1 (𝜑 → (𝑥𝐴𝐵) = (𝑥𝐴𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wcel 2107  cmpt 5187
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-opab 5167  df-mpt 5188
This theorem is referenced by:  ofeqd  7612  mpocurryvald  8194  rdgeq1  8350  rdgeq2  8351  omv  8451  oev  8453  oieq1  9407  oieq2  9408  cantnflem1  9584  wunex2  10633  wuncval2  10642  rpnnen1  12863  seqof2  13921  relexpsucnnr  14870  relexp1g  14871  limsupval  15316  sumeq2w  15537  sumeq2ii  15538  cbvsum  15540  summo  15562  fsum  15565  fsumrlim  15656  fsumo1  15657  prodeq2w  15755  prodmo  15779  fprod  15784  bpolylem  15891  rpnnen2lem1  16056  rpnnen2lem2  16057  1arithlem1  16755  vdwapval  16805  vdwlem6  16818  vdwlem8  16820  vdwlem9  16821  vdwlem10  16822  ramub1lem2  16859  ramcl  16861  sloteq  17015  prdsplusgval  17315  prdsmulrval  17317  prdsdsval  17320  prdsvscaval  17321  ismon  17576  fucco  17811  curf1  18074  curf2  18078  yonedalem4a  18124  smndex1gbas  18672  smndex1gid  18673  grplactfval  18807  galactghm  19145  pmtrval  19192  sylow1  19344  sylow2b  19364  sylow3lem5  19372  sylow3  19374  iscyg  19615  gsumzaddlem  19657  gsumzmhm  19673  ablfac2  19827  gsumdixp  19986  zncyg  20908  phllmhm  20989  isphld  21011  frlmgsum  21131  frlmipval  21138  frlmphl  21140  uvcval  21144  fczpsrbag  21278  psrmulfval  21306  mvrval  21342  subrgmvr  21386  mplcoe1  21390  mplcoe3  21391  mplcoe5  21393  mplmon2  21421  subrgascl  21426  evlslem2  21441  evlslem3  21442  evlslem1  21444  mpfrcl  21447  evlsval  21448  evlsvar  21452  mpfind  21469  selvfval  21479  selvval  21480  mhpfval  21481  coe1fval  21528  pf1ind  21673  evl1gsumadd  21676  mamuval  21687  mamufv  21688  matgsum  21738  madetsumid  21762  mat1dimmul  21777  mvmulval  21844  mvmulfv  21845  mavmulfv  21847  1mavmul  21849  marepvval0  21867  mulmarep1gsum1  21874  mdetleib  21888  mdetleib2  21889  mdetfval1  21891  mdetleib1  21892  mdet0pr  21893  m1detdiag  21898  mdetralt  21909  mdetunilem9  21921  m2detleib  21932  smadiadetlem3  21969  mat2pmatmul  22032  decpmatmul  22073  decpmatmulsumfsupp  22074  pmatcollpw1  22077  monmatcollpw  22080  pmatcollpw3lem  22084  pmatcollpw3fi1lem2  22088  pm2mpval  22096  pm2mpfval  22097  mply1topmatval  22105  mp2pm2mplem1  22107  mp2pm2mplem3  22109  ptbasfi  22884  ptcnplem  22924  ptrescn  22942  cnmpt2k  22991  xkohmeo  23118  fmval  23246  fmf  23248  ptcmpg  23360  tmdmulg  23395  prdstmdd  23427  tsmspropd  23435  prdsxmslem2  23837  metdsval  24162  fsumcn  24185  expcn  24187  lebnumlem3  24278  pcoval  24326  pi1xfrcnv  24372  cphsscph  24567  rrxds  24709  rrxmval  24721  itg11  25007  mbfi1fseqlem2  25033  mbfi1fseqlem6  25037  mbfi1fseq  25038  mbfi1flimlem  25039  mbfmullem  25042  itg2const  25057  itg2mulc  25064  itg2monolem1  25067  itg2i1fseqle  25071  itg2i1fseq  25072  itg2addlem  25075  itg2cnlem1  25078  itg2cn  25080  isibl  25082  isibl2  25083  iblitg  25085  itgz  25097  itgvallem  25101  itgvallem3  25102  iblcnlem1  25104  itgcnlem  25106  iblrelem  25107  iblposlem  25108  iblpos  25109  itgrevallem1  25111  itgposval  25112  iblss2  25122  itgss  25128  itgfsum  25143  iblabslem  25144  iblmulc2  25147  bddmulibl  25155  itgcn  25161  ellimc  25189  dvnfval  25238  cpnfval  25248  dvexp  25269  dvexp2  25270  dvmptfsum  25291  dvlipcn  25310  dvivthlem1  25324  dvfsumle  25337  dvfsumabs  25339  dvfsumlem2  25343  itgpowd  25366  elply2  25509  elplyr  25514  elplyd  25515  coeeu  25538  coelem  25539  coeeq  25540  plyco  25554  coe11  25566  coe1termlem  25571  dgrcolem1  25586  dvply2g  25597  elqaalem3  25633  eltayl  25671  tayl0  25673  taylthlem1  25684  taylthlem2  25685  ulmcau  25706  ulmdvlem1  25711  ulmdvlem3  25713  mtest  25715  mtestbdd  25716  pserval  25721  pserulm  25733  psercn  25737  pserdvlem2  25739  abelthlem3  25744  logtayl  25967  dvcxp1  26045  dvcncxp1  26048  logbmpt  26090  dmarea  26259  lgamgulmlem2  26331  lgamgulmlem5  26334  musum  26492  dchrptlem2  26565  dchrptlem3  26566  dchrpt  26567  lgsval  26601  lgsval4lem  26608  lgsneg  26621  lgsmod  26623  rpvmasum2  26812  padicfval  26916  ostth2  26937  ostth3  26938  ostth  26939  lmif  27556  islmib  27558  incistruhgr  27859  eucrct2eupth  29018  htthlem  29688  htth  29689  pjhfval  30167  hosmval  30506  hommval  30507  hodmval  30508  hfsmval  30509  hfmmval  30510  brafval  30714  kbfval  30723  mptprop  31438  psgnfzto1st  31779  linds2eq  31992  elrspunidl  32023  lbsdiflsp0  32135  fedgmullem1  32138  fedgmullem2  32139  fedgmul  32140  mdetpmtr1  32208  zar0ring  32263  ordtcnvNEW  32305  ordtrest2NEW  32308  xrhval  32403  indval  32416  esum2dlem  32495  ofceq  32500  itgeq12dv  32730  ballotlemfval  32893  vtsval  33054  lpadval  33093  ptpconn  33631  cvmliftlem15  33696  cvmlift2lem4  33704  cvmlift2  33714  snmlval  33729  snmlflim  33730  satf  33751  mrsubfval  33906  mrsubrn  33911  elmsubrn  33926  msubrn  33927  msubco  33929  faclim  34129  faclim2  34131  knoppcnlem1  34888  knoppcnlem6  34893  knoppcnlem7  34894  bj-evaleq  35475  csbrdgg  35732  curfv  35990  matunitlindflem2  36007  poimirlem5  36015  poimirlem6  36016  poimirlem7  36017  poimirlem8  36018  poimirlem10  36020  poimirlem11  36021  poimirlem12  36022  poimirlem15  36025  poimirlem16  36026  poimirlem17  36027  poimirlem18  36028  poimirlem19  36029  poimirlem20  36030  poimirlem21  36031  poimirlem22  36032  poimirlem27  36037  voliunnfl  36054  itg2addnclem  36061  itg2addnclem3  36063  itg2addnc  36064  itg2gt0cn  36065  iblabsnclem  36073  iblmulc2nc  36075  ftc1anclem2  36084  ftc1anclem6  36088  ftc1anclem8  36090  ftc1anc  36091  ftc2nc  36092  upixp  36120  rrncmslem  36223  ismrer1  36229  tendoplcbv  39170  tendopl  39171  tendoicbv  39188  tendoi  39189  dihfval  39626  lcfl7N  39896  lcfrlem8  39944  lcfrlem9  39945  lcf1o  39946  hvmapval  40155  hdmap1fval  40191  hdmapffval  40221  hdmapfval  40222  hgmapffval  40280  hgmapfval  40281  lcmineqlem7  40424  lcmineqlem12  40429  evlsbagval  40664  fsuppind  40668  fsuppssindlem2  40670  fsuppssind  40671  mzpclval  40951  mzpcl2  40956  mzpexpmpt  40971  mzpsubst  40974  mzpcompact2lem  40977  rmxfval  41130  rmyfval  41131  aomclem8  41291  hbtlem1  41353  hbtlem7  41355  rfovfvd  42179  fsovrfovd  42186  fsovfvd  42187  fsovcnvlem  42190  dssmapfv2d  42195  dssmapnvod  42197  ntrneibex  42250  mnringmulrvald  42412  mnringmulrcld  42413  expgrowthi  42518  expgrowth  42520  binomcxplemdvsum  42540  addrval  42651  subrval  42652  mulvval  42653  fmulcl  43717  fmuldfeqlem1  43718  fprodcnlem  43735  fprodcn  43736  fnlimfv  43799  fnlimcnv  43803  fnlimfvre  43810  fnlimfvre2  43813  fnlimf  43814  fnlimabslt  43815  liminfval  43895  limsupresxr  43902  liminfresxr  43903  liminfvalxr  43919  fprodcncf  44036  dvnmptdivc  44074  dvnxpaek  44078  dvnmul  44079  dvmptfprod  44081  dvnprodlem1  44082  dvnprodlem2  44083  dvnprodlem3  44084  dvnprod  44085  stoweidlem2  44138  stoweidlem17  44153  stoweidlem19  44155  stoweidlem20  44156  stoweidlem43  44179  stoweidlem62  44198  stoweid  44199  dirkercncflem2  44240  fourierdlem112  44354  fourierdlem113  44355  etransclem1  44371  etransclem5  44375  etransclem17  44387  etransclem19  44389  etransclem22  44392  sge0val  44502  ovnlecvr  44694  ovncvrrp  44700  ovn0lem  44701  ovnsubaddlem1  44706  ovnsubadd  44708  hsphoif  44712  hsphoival  44715  hoidmv1lelem1  44727  hoidmv1lelem2  44728  hoidmv1lelem3  44729  hoidmv1le  44730  hoidmvlelem1  44731  hoidmvlelem2  44732  hoidmvlelem3  44733  hoidmvlelem4  44734  hoidmvlelem5  44735  hoidmvle  44736  ovnhoilem1  44737  ovnhoi  44739  hoidifhspval  44744  ovncvr2  44747  hoidifhspval2  44751  hspmbllem2  44763  hspmbllem3  44764  hspmbl  44765  ovnovollem1  44792  vonioolem2  44817  vonioo  44818  vonicclem2  44820  vonicc  44821  smflimlem4  44910  smflim  44913  smflim2  44942  smfsuplem2  44948  smfsup  44950  smfinf  44954  smflimsuplem2  44957  smflimsuplem5  44960  smflimsuplem7  44962  smflimsup  44964  cfsetsnfsetfo  45189  c0rhm  46105  c0rnghm  46106  lincop  46384  1arymaptfv  46621  itcoval  46642  itcovalpc  46653  itcovalt2  46658  ackvalsuc1mpt  46659  ackval1  46662  aacllem  47143
  Copyright terms: Public domain W3C validator