Theorem cbvmptv 5208

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 5209 for a less restrictive version requiring more axioms. (Revised by GG, 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.

Step	Hyp	Ref	Expression
1		eleq1w 2848	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2776	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 643	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5182	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5186	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5186	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2798	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1563   ∈ wcel 2145  {copab 5166   ↦ cmpt 5185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-opab 5167  df-mpt 5186

This theorem is referenced by:  fnmptfvd  7026  mptcnfimad  7971  onnseq  8319  rdgsucmpt2  8405  frsucmpt2  8415  fsetfocdm  8846  fsetprcnex  8847  resixpfo  8922  pw2f1olem  9057  xpmapen  9121  dffi3  9379  ordtypecbv  9467  inf3lema  9581  cantnflem1  9646  cnfcomlem  9656  infxpenc2  9994  fseqenlem1  9996  dfac8a  10002  dfac12r  10118  r1om  10214  fictb  10215  cfsmo  10243  coftr  10245  fin23lem38  10321  compsscnv  10343  isf34lem1  10344  compss  10348  fin1a2lem1  10372  fin1a2lem3  10374  fin1a2lem13  10384  itunisuc  10391  hsmex  10404  domtriom  10415  axdc2  10421  zorn2g  10475  ttukey2g  10488  axdc  10493  konigth  10542  pwcfsdom  10556  canthp1  10627  wunex2  10711  wuncval2  10720  negiso  12183  infrenegsup  12186  rpnnen1  12995  caurcvg2  15717  caucvg  15718  summo  15756  zsum  15757  fsum  15759  ackbijnn  15870  cbvprodv  15956  prodmo  15978  zprod  15979  fprod  15983  iprodmul  16045  bpolyval  16091  phimullem  16826  eulerth  16830  iserodd  16883  prmreclem5  16968  prmrec  16970  vdwlem7  17035  vdwlem9  17037  vdwlem10  17038  ramub1  17076  ramcl  17077  yonedalem4c  18321  yonedalem3b  18323  gsumwspan  18893  smndex1iidm  18948  smndex1gid  18951  smndex1gidOLD  18952  smndex2dlinvh  18967  grplactcnv  19097  gicqusker  19346  galactghm  19462  symgfixfo  19497  pmtrdifwrdel  19543  pmtrdifwrdel2  19544  odf1o2  19631  sylow1lem2  19657  sylow1  19661  sylow2b  19681  sylow3lem1  19685  sylow3lem5  19689  sylow3  19691  efgtf  19780  efgsval  19789  ghmcyg  19954  cycsubgcyg  19959  ablfaclem3  20147  ablfac2  20149  srgbinomlem4  20299  funcrngcsetcALT  20714  fidomndrnglem  20842  isphld  21761  frlmphl  21888  mplmonmul  22144  evlslem2  22187  mat1ric  22601  mdetralt  22722  smadiadetlem3  22782  pmatcollpw3lem  22897  mp2pm2mplem5  22924  mp2pm2mp  22925  pm2mpmhmlem2  22933  cpmidpmat  22987  cpmadugsumlemF  22990  cpmadugsumfi  22991  cpmadumatpoly  22997  chcoeffeqlem  22999  cayleyhamilton0  23003  cayleyhamilton  23004  cayleyhamiltonALT  23005  cayleyhamilton1  23006  ordtbaslem  23302  ordtbas2  23305  lly1stc  23610  ptpjopn  23726  xkohmeo  23929  fbasrn  23998  elfm  24061  tmdmulg  24206  tmdgsum  24209  qustgpopn  24234  tsmsfbas  24242  tsmsf1o  24259  ustuqtoplem  24353  utopsnneip  24362  fmucnd  24405  ucnextcn  24417  met1stc  24635  prdsxmslem2  24643  metustto  24667  metustexhalf  24670  metuust  24674  cfilucfil2  24675  metuel  24678  metuel2  24679  psmetutop  24681  restmetu  24684  metucn  24685  xrge0tsms  24949  metdsge  24964  expcn  24988  pi1xfrcnv  25173  minveclem3b  25544  minveclem5  25549  minvec  25552  ovollb2  25605  ovolshftlem2  25626  ovolscalem2  25630  ovolicc  25639  ioombl1  25678  uniioombllem6  25704  volsup2  25721  vitali  25729  mbfi1fseq  25837  mbfmullem  25841  itg2seq  25858  itg2i1fseq  25871  itg2addlem  25874  itg2cnlem1  25877  itg2cn  25879  cbvitgv  25893  dvfsumrlimge0  26146  plyadd  26331  plymul  26332  coeeu  26339  coeid  26352  dvply2g  26403  plydivex  26415  elqaalem2  26438  elqaa  26440  taylthlem1  26490  taylth  26492  pserval  26527  radcnvlem2  26531  radcnvlt2  26536  dvradcnv  26538  pserulm  26539  psercn  26543  pserdvlem2  26545  pserdv  26546  efgh  26660  eff1olem  26667  circgrp  26671  circsubm  26672  logno1  26755  emcl  27121  harmonicbnd  27122  harmonicbnd2  27123  basel  27208  musum  27309  dchr1  27375  dchrptlem2  27383  dchrpt  27385  lgsqrlem4  27467  lgseisenlem3  27495  2sqlem1  27535  dchrmusumlema  27611  dchrmusum2  27612  dchrvmasumlema  27618  dchrvmasumiflem1  27619  dchrisum0ff  27625  dchrisum0lema  27632  dchrisum0lem1b  27633  dchrisum0lem2a  27635  nosupcbv  27820  noinfcbv  27835  precsexlemcbv  28353  seqsfn  28456  seqsp1  28458  wlknwwlksnbij  30142  clwlkclwwlken  30268  clwlknf1oclwwlkn  30340  frgrncvvdeqlem8  30562  frgrncvvdeqlem9  30563  numclwwlk1lem2  30616  ubthlem3  31129  minveco  31141  htth  31175  fsuppcurry1  32977  fsuppcurry2  32978  gsumhashmul  33295  gsummulsubdishift1  33296  gsummulsubdishift1s  33298  gsummulsubdishift2s  33299  xrge0tsmsd  33301  elrgspnlem1  33470  elrgspnlem2  33471  elrgspn  33474  elrgspnsubrunlem1  33475  elrgspnsubrunlem2  33476  elrgspnsubrun  33477  idomsubr  33540  nsgmgc  33632  nsgqusf1olem1  33633  lmicqusker  33638  ricqusker  33646  elrspunidl  33647  elrspunsn  33648  zringfrac  33756  0mplric  33817  selvply1rhmlemb  33821  selvply1rhmlem3  33824  selvply1rhmlem5  33826  selvply1rhm  33827  mplidom  33830  mplvrpmga  33847  mplvrpmrhm  33849  psrgsum  33850  psrmonmul  33852  psrmonprod  33854  splysubrg  33862  issply  33863  esplyfvaln  33876  vietalem  33881  vieta  33882  ply1degltdim  33925  lbsdiflsp0  33928  fedgmullem1  33931  fedgmul  33933  assarrginv  33938  evls1fldgencl  33972  fldextrspunlsplem  33975  fldextrspunlsp  33976  extdgfialglem2  33995  extdgfialg  33996  algextdeglem4  34022  algextdeg  34027  constrcbvlem  34057  madjusmdetlem2  34130  madjusmdet  34133  zartop  34178  zartopon  34179  zart0  34181  zarmxt1  34182  zarcmp  34184  rhmpreimacn  34187  xrge0mulc1cn  34243  xrge0tmd  34247  xrge0tmdALT  34248  cbvesumv  34345  gsumesum  34361  esumlub  34362  esumpcvgval  34380  esumcvg  34388  esumcvg2  34389  eulerpartlems  34662  eulerpart  34684  fibp1  34703  rrvadd  34754  ballotlemfval  34792  ballotlemi  34803  ballotlemsval  34811  ballotlemsv  34812  ballotlemsf1o  34816  ballotlemrval  34820  ballotlemrinv  34836  signsply0  34850  actfunsnf1o  34903  actfunsnrndisj  34904  itgexpif  34905  hgt750lemb  34955  onvf1odlem3  35455  derangfmla  35548  erdsze  35560  pconnpi1  35595  cvmscbv  35616  cvmsss2  35632  cvmliftlem15  35656  cvmlift2  35674  cvmlift3  35686  elmrsubrn  35878  iprodefisum  36099  cbvprodvw2  36615  cbvitgvw2  36616  knoppcnlem7  36945  knoppf  36981  f1omptsn  37838  mptsnun  37840  fin2so  38113  poimirlem27  38153  broucube  38160  ftc1anclem5  38203  ftc1anclem6  38204  sdclem2  38248  prdstotbnd  38300  prdsbnd2  38301  heiborlem10  38326  lshpkrcl  39747  tendoplcbv  41406  tendo0cbv  41417  tendoicbv  41424  lcfl7N  42132  lcf1o  42182  hdmap1cbv  42433  frlmsnic  43165  evlselv  43178  mzpclval  43313  mzpcompact2lem  43339  rmxyval  43499  dnnumch1  43628  aomclem3  43640  aomclem8  43645  dfac21  43650  pwfi2f1o  43680  dftrcl3  44303  dfrtrcl3  44316  rfovcnvf1od  44587  fsovrfovd  44592  fsovcnvlem  44596  dssmapnvod  44603  clsk3nimkb  44623  radcnvrat  44883  expgrowthi  44902  expgrowth  44904  dvradcnv2  44916  binomcxplemradcnv  44921  binomcxplemdvbinom  44922  binomcxplemdvsum  44924  binomcxplemnotnn0  44925  binomcxp  44926  wessf1ornlem  45762  projf1o  45773  fsumsermpt  46154  fmuldfeqlem1  46157  fprodcn  46175  sumnnodd  46205  limsupvaluz  46281  limsupvaluz2  46311  supcnvlimsup  46313  supcnvlimsupmpt  46314  liminfval2  46341  liminflelimsuplem  46348  fprodsubrecnncnv  46481  fprodaddrecnncnv  46483  dvsinax  46486  fperdvper  46492  dvcosax  46499  ioodvbdlimc1lem1  46504  ioodvbdlimc1  46506  ioodvbdlimc2  46508  dvnmul  46516  dvnprodlem1  46519  dvnprodlem2  46520  dvnprodlem3  46521  dvnprod  46522  itgsin0pilem1  46523  itgiccshift  46553  stoweidlem2  46575  stoweidlem17  46590  stoweidlem32  46605  stoweidlem34  46607  stoweidlem43  46616  stirlinglem2  46648  stirlinglem3  46649  stirlinglem8  46654  dirkerval  46664  dirkerval2  46667  dirkeritg  46675  dirkercncflem3  46678  dirkercncf  46680  fourierdlem14  46694  fourierdlem18  46698  fourierdlem53  46732  fourierdlem62  46741  fourierdlem71  46750  fourierdlem74  46753  fourierdlem75  46754  fourierdlem76  46755  fourierdlem80  46759  fourierdlem81  46760  fourierdlem84  46763  fourierdlem88  46767  fourierdlem92  46771  fourierdlem93  46772  fourierdlem94  46773  fourierdlem95  46774  fourierdlem96  46775  fourierdlem97  46776  fourierdlem98  46777  fourierdlem99  46778  fourierdlem101  46780  fourierdlem103  46782  fourierdlem104  46783  fourierdlem105  46784  fourierdlem106  46785  fourierdlem107  46786  fourierdlem108  46787  fourierdlem110  46789  fourierdlem111  46790  fourierdlem112  46791  fourierdlem113  46792  fourierdlem115  46794  fouriersw  46804  elaa2  46807  etransclem1  46808  etransclem5  46812  etransclem6  46813  etransclem11  46818  etransclem13  46820  etransclem41  46848  etransclem47  46854  etransc  46856  ioorrnopn  46878  ioorrnopnxr  46880  subsaliuncl  46931  sge0resplit  46979  sge0fodjrnlem  46989  nnfoctbdj  47029  iundjiun  47033  voliunsge0lem  47045  meaiuninclem  47053  meaiuninc  47054  meaiininclem  47059  meaiininc  47060  omeiunltfirp  47092  carageniuncllem2  47095  carageniuncl  47096  0ome  47102  isomennd  47104  hoicvrrex  47129  ovn0  47139  ovnsubaddlem2  47144  ovnsubadd  47145  sge0hsphoire  47162  hoidmv1lelem3  47166  hoidmv1le  47167  hoidmvlelem1  47168  hoidmvlelem2  47169  hoidmvlelem3  47170  hoidmvlelem4  47171  hoidmvlelem5  47172  hoidmvle  47173  ovnhoilem2  47175  ovnhoi  47176  hspmbllem2  47200  hspmbl  47202  hoimbl  47204  opnvonmbllem2  47206  ovnsubadd2  47219  ovolval4  47224  ovolval5lem3  47227  ovnovollem3  47231  iccvonmbl  47252  vonioolem2  47254  vonioo  47255  vonicclem2  47257  vonicc  47258  smflimlem4  47347  smfsuplem2  47385  smflimsuplem1  47393  smflimsuplem8  47400  smflimsup  47401  fundcmpsurbijinjpreimafv  48012  prproropf1o  48112  isuspgrim0  48515  cycldlenngric  48549  isubgr3stgrlem8  48594  rmsupp0  49000  domnmsuppn0  49001  rmsuppss  49002  suppmptcfin  49008  ply1mulgsum  49022  lcoc0  49054  linc1  49057  lcoel0  49060  lcoss  49068  el0ldep  49098  lincresunit3  49113  isldepslvec2  49117  itcovalpclem2  49303  itcovalt2lem2  49308  amgmlemALT  50433