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

Theorem cbvmptv 5216
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid auxiliary axioms . See cbvmptvg 5218 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Nov-2024.)
Hypothesis
Ref Expression
cbvmptv.1 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbvmptv (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑦,𝐵   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbvmptv
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eleq1w 2820 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2 cbvmptv.1 . . . . 5 (𝑥 = 𝑦𝐵 = 𝐶)
32eqeq2d 2747 . . . 4 (𝑥 = 𝑦 → (𝑧 = 𝐵𝑧 = 𝐶))
41, 3anbi12d 631 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝑧 = 𝐵) ↔ (𝑦𝐴𝑧 = 𝐶)))
54cbvopab1v 5182 . 2 {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
6 df-mpt 5187 . 2 (𝑥𝐴𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥𝐴𝑧 = 𝐵)}
7 df-mpt 5187 . 2 (𝑦𝐴𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦𝐴𝑧 = 𝐶)}
85, 6, 73eqtr4i 2774 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  {copab 5165  cmpt 5186
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3406  df-v 3445  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-sn 4585  df-pr 4587  df-op 4591  df-opab 5166  df-mpt 5187
This theorem is referenced by:  fnmptfvd  6988  onnseq  8286  rdgsucmpt2  8372  frsucmpt2  8382  fsetfocdm  8795  fsetprcnex  8796  resixpfo  8870  pw2f1olem  9016  xpmapen  9085  dffi3  9363  ordtypecbv  9449  inf3lema  9556  cantnflem1  9621  cnfcomlem  9631  infxpenc2  9954  fseqenlem1  9956  dfac8a  9962  dfac12r  10078  r1om  10176  fictb  10177  cfsmo  10203  coftr  10205  fin23lem38  10281  compsscnv  10303  isf34lem1  10304  compss  10308  fin1a2lem1  10332  fin1a2lem3  10334  fin1a2lem13  10344  itunisuc  10351  hsmex  10364  domtriom  10375  axdc2  10381  zorn2g  10435  ttukey2g  10448  axdc  10453  konigth  10501  pwcfsdom  10515  canthp1  10586  wunex2  10670  wuncval2  10679  negiso  12131  infrenegsup  12134  rpnnen1  12900  caurcvg2  15554  caucvg  15555  summo  15594  zsum  15595  fsum  15597  ackbijnn  15705  prodmo  15811  zprod  15812  fprod  15816  iprodmul  15878  bpolyval  15924  phimullem  16643  eulerth  16647  iserodd  16699  prmreclem5  16784  prmrec  16786  vdwlem7  16851  vdwlem9  16853  vdwlem10  16854  ramub1  16892  ramcl  16893  yonedalem4c  18158  yonedalem3b  18160  gsumwspan  18648  smndex1iidm  18703  smndex1gid  18705  smndex2dlinvh  18719  grplactcnv  18841  galactghm  19177  symgfixfo  19212  pmtrdifwrdel  19258  pmtrdifwrdel2  19259  odf1o2  19346  sylow1lem2  19372  sylow1  19376  sylow2b  19396  sylow3lem1  19400  sylow3lem5  19404  sylow3  19406  efgtf  19495  efgsval  19504  ghmcyg  19664  cycsubgcyg  19669  ablfaclem3  19857  ablfac2  19859  srgbinomlem4  19946  fidomndrnglem  20762  isphld  21043  frlmphl  21172  mplmonmul  21421  evlslem2  21473  mat1ric  21820  mdetralt  21941  smadiadetlem3  22001  pmatcollpw3lem  22116  mp2pm2mplem5  22143  mp2pm2mp  22144  pm2mpmhmlem2  22152  cpmidpmat  22206  cpmadugsumlemF  22209  cpmadugsumfi  22210  cpmadumatpoly  22216  chcoeffeqlem  22218  cayleyhamilton0  22222  cayleyhamilton  22223  cayleyhamiltonALT  22224  cayleyhamilton1  22225  ordtbaslem  22523  ordtbas2  22526  lly1stc  22831  ptpjopn  22947  xkohmeo  23150  fbasrn  23219  elfm  23282  tmdmulg  23427  tmdgsum  23430  qustgpopn  23455  tsmsfbas  23463  tsmsf1o  23480  ustuqtoplem  23575  utopsnneip  23584  fmucnd  23628  ucnextcn  23640  met1stc  23861  prdsxmslem2  23869  metustto  23893  metustexhalf  23896  metuust  23900  cfilucfil2  23901  metuel  23904  metuel2  23905  psmetutop  23907  restmetu  23910  metucn  23911  xrge0tsms  24181  metdsge  24196  expcn  24219  pi1xfrcnv  24404  minveclem3b  24776  minveclem5  24781  minvec  24784  ovollb2  24837  ovolshftlem2  24858  ovolscalem2  24862  ovolicc  24871  ioombl1  24910  uniioombllem6  24936  volsup2  24953  vitali  24961  mbfi1fseq  25070  mbfmullem  25074  itg2seq  25091  itg2i1fseq  25104  itg2addlem  25107  itg2cnlem1  25110  itg2cn  25112  dvfsumrlimge0  25378  plyadd  25562  plymul  25563  coeeu  25570  coeid  25583  dvply2g  25629  plydivex  25641  elqaalem2  25664  elqaa  25666  taylthlem1  25716  taylth  25718  pserval  25753  radcnvlem2  25757  radcnvlt2  25762  dvradcnv  25764  pserulm  25765  psercn  25769  pserdvlem2  25771  pserdv  25772  efgh  25881  eff1olem  25888  circgrp  25892  circsubm  25893  logno1  25975  emcl  26336  harmonicbnd  26337  harmonicbnd2  26338  basel  26423  musum  26524  dchr1  26589  dchrptlem2  26597  dchrpt  26599  lgsqrlem4  26681  lgseisenlem3  26709  2sqlem1  26749  dchrmusumlema  26825  dchrmusum2  26826  dchrvmasumlema  26832  dchrvmasumiflem1  26833  dchrisum0ff  26839  dchrisum0lema  26846  dchrisum0lem1b  26847  dchrisum0lem2a  26849  nosupcbv  27034  noinfcbv  27049  wlknwwlksnbij  28719  clwlkclwwlken  28842  clwlknf1oclwwlkn  28914  frgrncvvdeqlem8  29136  frgrncvvdeqlem9  29137  numclwwlk1lem2  29190  ubthlem3  29700  minveco  29712  htth  29746  fsuppcurry1  31525  fsuppcurry2  31526  gsumhashmul  31781  xrge0tsmsd  31782  nsgmgc  32073  nsgqusf1olem1  32074  elrspunidl  32082  lbsdiflsp0  32198  fedgmullem1  32201  fedgmul  32203  madjusmdetlem2  32278  madjusmdet  32281  zartop  32326  zartopon  32327  zart0  32329  zarmxt1  32330  zarcmp  32332  rhmpreimacn  32335  xrge0mulc1cn  32391  xrge0tmd  32395  xrge0tmdALT  32396  gsumesum  32527  esumlub  32528  esumpcvgval  32546  esumcvg  32554  esumcvg2  32555  eulerpartlems  32829  eulerpart  32851  fibp1  32870  rrvadd  32921  ballotlemfval  32958  ballotlemi  32969  ballotlemsval  32977  ballotlemsv  32978  ballotlemsf1o  32982  ballotlemrval  32986  ballotlemrinv  33002  signsply0  33032  actfunsnf1o  33086  actfunsnrndisj  33087  itgexpif  33088  hgt750lemb  33138  derangfmla  33653  erdsze  33665  pconnpi1  33700  cvmscbv  33721  cvmsss2  33737  cvmliftlem15  33761  cvmlift2  33779  cvmlift3  33791  elmrsubrn  33983  iprodefisum  34184  knoppcnlem7  34929  knoppf  34965  f1omptsn  35775  mptsnun  35777  fin2so  36032  poimirlem27  36072  broucube  36079  ftc1anclem5  36122  ftc1anclem6  36123  sdclem2  36168  prdstotbnd  36220  prdsbnd2  36221  heiborlem10  36246  lshpkrcl  37545  tendoplcbv  39205  tendo0cbv  39216  tendoicbv  39223  lcfl7N  39931  lcf1o  39981  hdmap1cbv  40232  frlmsnic  40689  mzpclval  40986  mzpcompact2lem  41012  rmxyval  41177  dnnumch1  41309  aomclem3  41321  aomclem8  41326  dfac21  41331  pwfi2f1o  41361  dftrcl3  41934  dfrtrcl3  41947  rfovcnvf1od  42218  fsovrfovd  42223  fsovcnvlem  42227  dssmapnvod  42234  clsk3nimkb  42254  radcnvrat  42536  expgrowthi  42555  expgrowth  42557  dvradcnv2  42569  binomcxplemradcnv  42574  binomcxplemdvbinom  42575  binomcxplemdvsum  42577  binomcxplemnotnn0  42578  binomcxp  42579  wessf1ornlem  43339  projf1o  43353  fsumsermpt  43752  fmuldfeqlem1  43755  fprodcn  43773  sumnnodd  43803  limsupvaluz  43881  limsupvaluz2  43911  supcnvlimsup  43913  supcnvlimsupmpt  43914  liminfval2  43941  liminflelimsuplem  43948  fprodsubrecnncnv  44081  fprodaddrecnncnv  44083  dvsinax  44086  fperdvper  44092  dvcosax  44099  ioodvbdlimc1lem1  44104  ioodvbdlimc1  44106  ioodvbdlimc2  44108  dvnmul  44116  dvnprodlem1  44119  dvnprodlem2  44120  dvnprodlem3  44121  dvnprod  44122  itgsin0pilem1  44123  itgiccshift  44153  stoweidlem2  44175  stoweidlem17  44190  stoweidlem32  44205  stoweidlem34  44207  stoweidlem43  44216  stirlinglem2  44248  stirlinglem3  44249  stirlinglem8  44254  dirkerval  44264  dirkerval2  44267  dirkeritg  44275  dirkercncflem3  44278  dirkercncf  44280  fourierdlem14  44294  fourierdlem18  44298  fourierdlem53  44332  fourierdlem62  44341  fourierdlem71  44350  fourierdlem74  44353  fourierdlem75  44354  fourierdlem76  44355  fourierdlem80  44359  fourierdlem81  44360  fourierdlem84  44363  fourierdlem88  44367  fourierdlem92  44371  fourierdlem93  44372  fourierdlem94  44373  fourierdlem95  44374  fourierdlem96  44375  fourierdlem97  44376  fourierdlem98  44377  fourierdlem99  44378  fourierdlem101  44380  fourierdlem103  44382  fourierdlem104  44383  fourierdlem105  44384  fourierdlem106  44385  fourierdlem107  44386  fourierdlem108  44387  fourierdlem110  44389  fourierdlem111  44390  fourierdlem112  44391  fourierdlem113  44392  fourierdlem115  44394  fouriersw  44404  elaa2  44407  etransclem1  44408  etransclem5  44412  etransclem6  44413  etransclem11  44418  etransclem13  44420  etransclem41  44448  etransclem47  44454  etransc  44456  ioorrnopn  44478  ioorrnopnxr  44480  subsaliuncl  44531  sge0resplit  44579  sge0fodjrnlem  44589  nnfoctbdj  44629  iundjiun  44633  voliunsge0lem  44645  meaiuninclem  44653  meaiuninc  44654  meaiininclem  44659  meaiininc  44660  omeiunltfirp  44692  carageniuncllem2  44695  carageniuncl  44696  0ome  44702  isomennd  44704  hoicvrrex  44729  ovn0  44739  ovnsubaddlem2  44744  ovnsubadd  44745  sge0hsphoire  44762  hoidmv1lelem3  44766  hoidmv1le  44767  hoidmvlelem1  44768  hoidmvlelem2  44769  hoidmvlelem3  44770  hoidmvlelem4  44771  hoidmvlelem5  44772  hoidmvle  44773  ovnhoilem2  44775  ovnhoi  44776  hspmbllem2  44800  hspmbl  44802  hoimbl  44804  opnvonmbllem2  44806  ovnsubadd2  44819  ovolval4  44824  ovolval5lem3  44827  ovnovollem3  44831  iccvonmbl  44852  vonioolem2  44854  vonioo  44855  vonicclem2  44857  vonicc  44858  smflimlem4  44947  smfsuplem2  44985  smflimsuplem1  44993  smflimsuplem8  45000  smflimsup  45001  fundcmpsurbijinjpreimafv  45531  prproropf1o  45631  funcrngcsetcALT  46229  rmsupp0  46376  domnmsuppn0  46377  rmsuppss  46378  suppmptcfin  46387  ply1mulgsum  46403  lcoc0  46435  linc1  46438  lcoel0  46441  lcoss  46449  el0ldep  46479  lincresunit3  46494  isldepslvec2  46498  itcovalpclem2  46689  itcovalt2lem2  46694  amgmlemALT  47182
  Copyright terms: Public domain W3C validator