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

Theorem cbvmptv 5166
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 ax-13 2385. See cbvmptvg 5167 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.)
Hypothesis
Ref Expression
cbvmptv.1 (𝑥 = 𝑦𝐵 = 𝐶)
Assertion
Ref Expression
cbvmptv (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Distinct variable groups:   𝑥,𝐴,𝑦   𝑦,𝐵   𝑥,𝐶
Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑦)

Proof of Theorem cbvmptv
StepHypRef Expression
1 nfcv 2982 . 2 𝑦𝐵
2 nfcv 2982 . 2 𝑥𝐶
3 cbvmptv.1 . 2 (𝑥 = 𝑦𝐵 = 𝐶)
41, 2, 3cbvmpt 5164 1 (𝑥𝐴𝐵) = (𝑦𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  cmpt 5143
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-opab 5126  df-mpt 5144
This theorem is referenced by:  fnmptfvd  6807  onnseq  7972  rdgsucmpt2  8057  frsucmpt2w  8066  frsucmpt2  8067  resixpfo  8489  pw2f1olem  8610  xpmapen  8674  dffi3  8884  ordtypecbv  8970  inf3lema  9076  cantnflem1  9141  cnfcomlem  9151  infxpenc2  9437  fseqenlem1  9439  dfac8a  9445  dfac12r  9561  r1om  9655  fictb  9656  cfsmo  9682  coftr  9684  fin23lem38  9760  compsscnv  9782  isf34lem1  9783  compss  9787  fin1a2lem1  9811  fin1a2lem3  9813  fin1a2lem13  9823  itunisuc  9830  hsmex  9843  domtriom  9854  axdc2  9860  zorn2g  9914  ttukey2g  9927  axdc  9932  konigth  9980  pwcfsdom  9994  canthp1  10065  wunex2  10149  wuncval2  10158  negiso  11610  infrenegsup  11613  rpnnen1  12372  caurcvg2  15024  caucvg  15025  summo  15064  zsum  15065  fsum  15067  ackbijnn  15173  prodmo  15280  zprod  15281  fprod  15285  iprodmul  15347  bpolyval  15393  phimullem  16106  eulerth  16110  iserodd  16162  prmreclem5  16246  prmrec  16248  vdwlem7  16313  vdwlem9  16315  vdwlem10  16316  ramub1  16354  ramcl  16355  yonedalem4c  17517  yonedalem3b  17519  gsumwspan  17994  grplactcnv  18132  galactghm  18451  symgfixfo  18487  pmtrdifwrdel  18533  pmtrdifwrdel2  18534  odf1o2  18618  sylow1lem2  18644  sylow1  18648  sylow2b  18668  sylow3lem1  18672  sylow3lem5  18676  sylow3  18678  efgtf  18768  efgsval  18777  ghmcyg  18936  cycsubgcyg  18941  ablfaclem3  19129  ablfac2  19131  srgbinomlem4  19213  fidomndrnglem  19998  mplmonmul  20163  evlslem2  20210  isphld  20714  frlmphl  20841  mat1ric  21012  mdetralt  21133  smadiadetlem3  21193  pmatcollpw3lem  21307  mp2pm2mplem5  21334  mp2pm2mp  21335  pm2mpmhmlem2  21343  cpmidpmat  21397  cpmadugsumlemF  21400  cpmadugsumfi  21401  cpmadumatpoly  21407  chcoeffeqlem  21409  cayleyhamilton0  21413  cayleyhamilton  21414  cayleyhamiltonALT  21415  cayleyhamilton1  21416  ordtbaslem  21712  ordtbas2  21715  lly1stc  22020  ptpjopn  22136  xkohmeo  22339  fbasrn  22408  elfm  22471  tmdmulg  22616  tmdgsum  22619  qustgpopn  22643  tsmsfbas  22651  tsmsf1o  22668  ustuqtoplem  22763  utopsnneip  22772  fmucnd  22816  ucnextcn  22828  met1stc  23046  prdsxmslem2  23054  metustto  23078  metustexhalf  23081  metuust  23085  cfilucfil2  23086  metuel  23089  metuel2  23090  psmetutop  23092  restmetu  23095  metucn  23096  xrge0tsms  23357  metdsge  23372  expcn  23395  pi1xfrcnv  23576  minveclem3b  23946  minveclem5  23951  minvec  23954  ovollb2  24005  ovolshftlem2  24026  ovolscalem2  24030  ovolicc  24039  ioombl1  24078  uniioombllem6  24104  volsup2  24121  vitali  24129  mbfi1fseq  24237  mbfmullem  24241  itg2seq  24258  itg2i1fseq  24271  itg2addlem  24274  itg2cnlem1  24277  itg2cn  24279  dvfsumrlimge0  24542  plyadd  24722  plymul  24723  coeeu  24730  coeid  24743  dvply2g  24789  plydivex  24801  elqaalem2  24824  elqaa  24826  taylthlem1  24876  taylth  24878  pserval  24913  radcnvlem2  24917  radcnvlt2  24922  dvradcnv  24924  pserulm  24925  psercn  24929  pserdvlem2  24931  pserdv  24932  efgh  25038  eff1olem  25045  circgrp  25049  circsubm  25050  logno1  25132  emcl  25494  harmonicbnd  25495  harmonicbnd2  25496  basel  25581  musum  25682  dchr1  25747  dchrptlem2  25755  dchrpt  25757  lgsqrlem4  25839  lgseisenlem3  25867  2sqlem1  25907  dchrmusumlema  25983  dchrmusum2  25984  dchrvmasumlema  25990  dchrvmasumiflem1  25991  dchrisum0ff  25997  dchrisum0lema  26004  dchrisum0lem1b  26005  dchrisum0lem2a  26007  wlknwwlksnbij  27580  clwlkclwwlken  27704  clwlknf1oclwwlkn  27777  frgrncvvdeqlem8  27999  frgrncvvdeqlem9  28000  numclwwlk1lem2  28053  ubthlem3  28563  minveco  28575  htth  28609  fsuppcurry1  30374  fsuppcurry2  30375  xrge0tsmsd  30606  lbsdiflsp0  30908  fedgmullem1  30911  fedgmul  30913  madjusmdetlem2  30979  madjusmdet  30982  xrge0mulc1cn  31070  xrge0tmd  31074  xrge0tmdALT  31075  gsumesum  31204  esumlub  31205  esumpcvgval  31223  esumcvg  31231  esumcvg2  31232  eulerpartlems  31504  eulerpart  31526  fibp1  31545  rrvadd  31596  ballotlemfval  31633  ballotlemi  31644  ballotlemsval  31652  ballotlemsv  31653  ballotlemsf1o  31657  ballotlemrval  31661  ballotlemrinv  31677  signsply0  31707  actfunsnf1o  31761  actfunsnrndisj  31762  itgexpif  31763  hgt750lemb  31813  derangfmla  32321  erdsze  32333  pconnpi1  32368  cvmscbv  32389  cvmsss2  32405  cvmliftlem15  32429  cvmlift2  32447  cvmlift3  32459  elmrsubrn  32651  iprodefisum  32857  trpredtr  32953  trpredmintr  32954  noeta  33106  knoppcnlem7  33722  knoppf  33758  f1omptsn  34487  mptsnun  34489  fin2so  34746  poimirlem27  34786  broucube  34793  ftc1anclem5  34838  ftc1anclem6  34839  sdclem2  34885  prdstotbnd  34940  prdsbnd2  34941  heiborlem10  34966  lshpkrcl  36119  tendoplcbv  37778  tendo0cbv  37789  tendoicbv  37796  lcfl7N  38504  lcf1o  38554  hdmap1cbv  38805  frlmsnic  39014  mzpclval  39187  mzpcompact2lem  39213  rmxyval  39377  dnnumch1  39509  aomclem3  39521  aomclem8  39526  dfac21  39531  pwfi2f1o  39561  dftrcl3  39930  dfrtrcl3  39943  rfovcnvf1od  40215  fsovrfovd  40220  fsovcnvlem  40224  dssmapnvod  40231  clsk3nimkb  40255  radcnvrat  40511  expgrowthi  40530  expgrowth  40532  dvradcnv2  40544  binomcxplemradcnv  40549  binomcxplemdvbinom  40550  binomcxplemdvsum  40552  binomcxplemnotnn0  40553  binomcxp  40554  wessf1ornlem  41310  projf1o  41324  fsumsermpt  41725  fmuldfeqlem1  41728  fprodcn  41746  sumnnodd  41776  limsupvaluz  41854  limsupvaluz2  41884  supcnvlimsup  41886  supcnvlimsupmpt  41887  liminfval2  41914  liminflelimsuplem  41921  fprodsubrecnncnv  42057  fprodaddrecnncnv  42059  dvsinax  42062  fperdvper  42068  dvcosax  42076  ioodvbdlimc1lem1  42081  ioodvbdlimc1  42083  ioodvbdlimc2  42085  dvnmul  42093  dvnprodlem1  42096  dvnprodlem2  42097  dvnprodlem3  42098  dvnprod  42099  itgsin0pilem1  42100  itgiccshift  42130  stoweidlem2  42153  stoweidlem17  42168  stoweidlem32  42183  stoweidlem34  42185  stoweidlem43  42194  stirlinglem2  42226  stirlinglem3  42227  stirlinglem8  42232  dirkerval  42242  dirkerval2  42245  dirkeritg  42253  dirkercncflem3  42256  dirkercncf  42258  fourierdlem14  42272  fourierdlem18  42276  fourierdlem53  42310  fourierdlem62  42319  fourierdlem71  42328  fourierdlem74  42331  fourierdlem75  42332  fourierdlem76  42333  fourierdlem80  42337  fourierdlem81  42338  fourierdlem84  42341  fourierdlem88  42345  fourierdlem92  42349  fourierdlem93  42350  fourierdlem94  42351  fourierdlem95  42352  fourierdlem96  42353  fourierdlem97  42354  fourierdlem98  42355  fourierdlem99  42356  fourierdlem101  42358  fourierdlem103  42360  fourierdlem104  42361  fourierdlem105  42362  fourierdlem106  42363  fourierdlem107  42364  fourierdlem108  42365  fourierdlem110  42367  fourierdlem111  42368  fourierdlem112  42369  fourierdlem113  42370  fourierdlem115  42372  fouriersw  42382  elaa2  42385  etransclem1  42386  etransclem5  42390  etransclem6  42391  etransclem11  42396  etransclem13  42398  etransclem41  42426  etransclem47  42432  etransc  42434  ioorrnopn  42456  ioorrnopnxr  42458  subsaliuncl  42507  sge0resplit  42554  sge0fodjrnlem  42564  nnfoctbdj  42604  iundjiun  42608  voliunsge0lem  42620  meaiuninclem  42628  meaiuninc  42629  meaiininclem  42634  meaiininc  42635  omeiunltfirp  42667  carageniuncllem2  42670  carageniuncl  42671  0ome  42677  isomennd  42679  hoicvrrex  42704  ovn0  42714  ovnsubaddlem2  42719  ovnsubadd  42720  sge0hsphoire  42737  hoidmv1lelem3  42741  hoidmv1le  42742  hoidmvlelem1  42743  hoidmvlelem2  42744  hoidmvlelem3  42745  hoidmvlelem4  42746  hoidmvlelem5  42747  hoidmvle  42748  ovnhoilem2  42750  ovnhoi  42751  hspmbllem2  42775  hspmbl  42777  hoimbl  42779  opnvonmbllem2  42781  ovnsubadd2  42794  ovolval4  42799  ovolval5lem3  42802  ovnovollem3  42806  iccvonmbl  42827  vonioolem2  42829  vonioo  42830  vonicclem2  42832  vonicc  42833  smflimlem4  42916  smfsuplem2  42952  smflimsuplem1  42960  smflimsuplem8  42967  smflimsup  42968  prproropf1o  43501  funcrngcsetcALT  44102  rmsupp0  44248  domnmsuppn0  44249  rmsuppss  44250  suppmptcfin  44259  ply1mulgsum  44276  lcoc0  44309  linc1  44312  lcoel0  44315  lcoss  44323  el0ldep  44353  lincresunit3  44368  isldepslvec2  44372  amgmlemALT  44736
  Copyright terms: Public domain W3C validator