Theorem cbvmptv 5195

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 5196 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 2814	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2742	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5169	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5173	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5173	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2764	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {copab 5153   ↦ cmpt 5172

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-opab 5154  df-mpt 5173

This theorem is referenced by:  fnmptfvd  6974  mptcnfimad  7918  onnseq  8264  rdgsucmpt2  8349  frsucmpt2  8359  fsetfocdm  8785  fsetprcnex  8786  resixpfo  8860  pw2f1olem  8994  xpmapen  9058  dffi3  9315  ordtypecbv  9403  inf3lema  9514  cantnflem1  9579  cnfcomlem  9589  infxpenc2  9910  fseqenlem1  9912  dfac8a  9918  dfac12r  10035  r1om  10131  fictb  10132  cfsmo  10159  coftr  10161  fin23lem38  10237  compsscnv  10259  isf34lem1  10260  compss  10264  fin1a2lem1  10288  fin1a2lem3  10290  fin1a2lem13  10300  itunisuc  10307  hsmex  10320  domtriom  10331  axdc2  10337  zorn2g  10391  ttukey2g  10404  axdc  10409  konigth  10457  pwcfsdom  10471  canthp1  10542  wunex2  10626  wuncval2  10635  negiso  12099  infrenegsup  12102  rpnnen1  12878  caurcvg2  15582  caucvg  15583  summo  15621  zsum  15622  fsum  15624  ackbijnn  15732  cbvprodv  15818  prodmo  15840  zprod  15841  fprod  15845  iprodmul  15907  bpolyval  15953  phimullem  16687  eulerth  16691  iserodd  16744  prmreclem5  16829  prmrec  16831  vdwlem7  16896  vdwlem9  16898  vdwlem10  16899  ramub1  16937  ramcl  16938  yonedalem4c  18180  yonedalem3b  18182  gsumwspan  18751  smndex1iidm  18806  smndex1gid  18808  smndex2dlinvh  18822  grplactcnv  18953  gicqusker  19198  galactghm  19314  symgfixfo  19349  pmtrdifwrdel  19395  pmtrdifwrdel2  19396  odf1o2  19483  sylow1lem2  19509  sylow1  19513  sylow2b  19533  sylow3lem1  19537  sylow3lem5  19541  sylow3  19543  efgtf  19632  efgsval  19641  ghmcyg  19806  cycsubgcyg  19811  ablfaclem3  19999  ablfac2  20001  srgbinomlem4  20145  funcrngcsetcALT  20554  fidomndrnglem  20685  isphld  21589  frlmphl  21716  mplmonmul  21969  evlslem2  22012  mat1ric  22400  mdetralt  22521  smadiadetlem3  22581  pmatcollpw3lem  22696  mp2pm2mplem5  22723  mp2pm2mp  22724  pm2mpmhmlem2  22732  cpmidpmat  22786  cpmadugsumlemF  22789  cpmadugsumfi  22790  cpmadumatpoly  22796  chcoeffeqlem  22798  cayleyhamilton0  22802  cayleyhamilton  22803  cayleyhamiltonALT  22804  cayleyhamilton1  22805  ordtbaslem  23101  ordtbas2  23104  lly1stc  23409  ptpjopn  23525  xkohmeo  23728  fbasrn  23797  elfm  23860  tmdmulg  24005  tmdgsum  24008  qustgpopn  24033  tsmsfbas  24041  tsmsf1o  24058  ustuqtoplem  24152  utopsnneip  24161  fmucnd  24204  ucnextcn  24216  met1stc  24434  prdsxmslem2  24442  metustto  24466  metustexhalf  24469  metuust  24473  cfilucfil2  24474  metuel  24477  metuel2  24478  psmetutop  24480  restmetu  24483  metucn  24484  xrge0tsms  24748  metdsge  24763  expcn  24788  expcnOLD  24790  pi1xfrcnv  24982  minveclem3b  25353  minveclem5  25358  minvec  25361  ovollb2  25415  ovolshftlem2  25436  ovolscalem2  25440  ovolicc  25449  ioombl1  25488  uniioombllem6  25514  volsup2  25531  vitali  25539  mbfi1fseq  25647  mbfmullem  25651  itg2seq  25668  itg2i1fseq  25681  itg2addlem  25684  itg2cnlem1  25687  itg2cn  25689  cbvitgv  25703  dvfsumrlimge0  25962  plyadd  26147  plymul  26148  coeeu  26155  coeid  26168  dvply2g  26217  dvply2gOLD  26218  plydivex  26230  elqaalem2  26253  elqaa  26255  taylthlem1  26306  taylth  26309  pserval  26344  radcnvlem2  26348  radcnvlt2  26353  dvradcnv  26355  pserulm  26356  psercn  26361  pserdvlem2  26363  pserdv  26364  efgh  26475  eff1olem  26482  circgrp  26486  circsubm  26487  logno1  26570  emcl  26938  harmonicbnd  26939  harmonicbnd2  26940  basel  27025  musum  27126  dchr1  27193  dchrptlem2  27201  dchrpt  27203  lgsqrlem4  27285  lgseisenlem3  27313  2sqlem1  27353  dchrmusumlema  27429  dchrmusum2  27430  dchrvmasumlema  27436  dchrvmasumiflem1  27437  dchrisum0ff  27443  dchrisum0lema  27450  dchrisum0lem1b  27451  dchrisum0lem2a  27453  nosupcbv  27639  noinfcbv  27654  precsexlemcbv  28142  seqsfn  28237  seqsp1  28239  wlknwwlksnbij  29864  clwlkclwwlken  29987  clwlknf1oclwwlkn  30059  frgrncvvdeqlem8  30281  frgrncvvdeqlem9  30282  numclwwlk1lem2  30335  ubthlem3  30847  minveco  30859  htth  30893  fsuppcurry1  32702  fsuppcurry2  32703  gsumhashmul  33036  xrge0tsmsd  33037  elrgspnlem1  33204  elrgspnlem2  33205  elrgspn  33208  elrgspnsubrunlem1  33209  elrgspnsubrunlem2  33210  elrgspnsubrun  33211  idomsubr  33270  nsgmgc  33372  nsgqusf1olem1  33373  lmicqusker  33378  ricqusker  33387  elrspunidl  33388  elrspunsn  33389  zringfrac  33514  mplvrpmga  33570  mplvrpmrhm  33572  splysubrg  33578  issply  33579  ply1degltdim  33631  lbsdiflsp0  33634  fedgmullem1  33637  fedgmul  33639  assarrginv  33644  evls1fldgencl  33678  fldextrspunlsplem  33681  fldextrspunlsp  33682  extdgfialglem2  33701  extdgfialg  33702  algextdeglem4  33728  algextdeg  33733  constrcbvlem  33763  madjusmdetlem2  33836  madjusmdet  33839  zartop  33884  zartopon  33885  zart0  33887  zarmxt1  33888  zarcmp  33890  rhmpreimacn  33893  xrge0mulc1cn  33949  xrge0tmd  33953  xrge0tmdALT  33954  cbvesumv  34051  gsumesum  34067  esumlub  34068  esumpcvgval  34086  esumcvg  34094  esumcvg2  34095  eulerpartlems  34368  eulerpart  34390  fibp1  34409  rrvadd  34460  ballotlemfval  34498  ballotlemi  34509  ballotlemsval  34517  ballotlemsv  34518  ballotlemsf1o  34522  ballotlemrval  34526  ballotlemrinv  34542  signsply0  34559  actfunsnf1o  34612  actfunsnrndisj  34613  itgexpif  34614  hgt750lemb  34664  onvf1odlem3  35137  derangfmla  35222  erdsze  35234  pconnpi1  35269  cvmscbv  35290  cvmsss2  35306  cvmliftlem15  35330  cvmlift2  35348  cvmlift3  35360  elmrsubrn  35552  iprodefisum  35773  cbvprodvw2  36280  cbvitgvw2  36281  knoppcnlem7  36532  knoppf  36568  f1omptsn  37370  mptsnun  37372  fin2so  37646  poimirlem27  37686  broucube  37693  ftc1anclem5  37736  ftc1anclem6  37737  sdclem2  37781  prdstotbnd  37833  prdsbnd2  37834  heiborlem10  37859  lshpkrcl  39154  tendoplcbv  40813  tendo0cbv  40824  tendoicbv  40831  lcfl7N  41539  lcf1o  41589  hdmap1cbv  41840  frlmsnic  42572  evlselv  42619  mzpclval  42757  mzpcompact2lem  42783  rmxyval  42947  dnnumch1  43076  aomclem3  43088  aomclem8  43093  dfac21  43098  pwfi2f1o  43128  dftrcl3  43752  dfrtrcl3  43765  rfovcnvf1od  44036  fsovrfovd  44041  fsovcnvlem  44045  dssmapnvod  44052  clsk3nimkb  44072  radcnvrat  44346  expgrowthi  44365  expgrowth  44367  dvradcnv2  44379  binomcxplemradcnv  44384  binomcxplemdvbinom  44385  binomcxplemdvsum  44387  binomcxplemnotnn0  44388  binomcxp  44389  wessf1ornlem  45221  projf1o  45233  fsumsermpt  45618  fmuldfeqlem1  45621  fprodcn  45639  sumnnodd  45669  limsupvaluz  45745  limsupvaluz2  45775  supcnvlimsup  45777  supcnvlimsupmpt  45778  liminfval2  45805  liminflelimsuplem  45812  fprodsubrecnncnv  45945  fprodaddrecnncnv  45947  dvsinax  45950  fperdvper  45956  dvcosax  45963  ioodvbdlimc1lem1  45968  ioodvbdlimc1  45970  ioodvbdlimc2  45972  dvnmul  45980  dvnprodlem1  45983  dvnprodlem2  45984  dvnprodlem3  45985  dvnprod  45986  itgsin0pilem1  45987  itgiccshift  46017  stoweidlem2  46039  stoweidlem17  46054  stoweidlem32  46069  stoweidlem34  46071  stoweidlem43  46080  stirlinglem2  46112  stirlinglem3  46113  stirlinglem8  46118  dirkerval  46128  dirkerval2  46131  dirkeritg  46139  dirkercncflem3  46142  dirkercncf  46144  fourierdlem14  46158  fourierdlem18  46162  fourierdlem53  46196  fourierdlem62  46205  fourierdlem71  46214  fourierdlem74  46217  fourierdlem75  46218  fourierdlem76  46219  fourierdlem80  46223  fourierdlem81  46224  fourierdlem84  46227  fourierdlem88  46231  fourierdlem92  46235  fourierdlem93  46236  fourierdlem94  46237  fourierdlem95  46238  fourierdlem96  46239  fourierdlem97  46240  fourierdlem98  46241  fourierdlem99  46242  fourierdlem101  46244  fourierdlem103  46246  fourierdlem104  46247  fourierdlem105  46248  fourierdlem106  46249  fourierdlem107  46250  fourierdlem108  46251  fourierdlem110  46253  fourierdlem111  46254  fourierdlem112  46255  fourierdlem113  46256  fourierdlem115  46258  fouriersw  46268  elaa2  46271  etransclem1  46272  etransclem5  46276  etransclem6  46277  etransclem11  46282  etransclem13  46284  etransclem41  46312  etransclem47  46318  etransc  46320  ioorrnopn  46342  ioorrnopnxr  46344  subsaliuncl  46395  sge0resplit  46443  sge0fodjrnlem  46453  nnfoctbdj  46493  iundjiun  46497  voliunsge0lem  46509  meaiuninclem  46517  meaiuninc  46518  meaiininclem  46523  meaiininc  46524  omeiunltfirp  46556  carageniuncllem2  46559  carageniuncl  46560  0ome  46566  isomennd  46568  hoicvrrex  46593  ovn0  46603  ovnsubaddlem2  46608  ovnsubadd  46609  sge0hsphoire  46626  hoidmv1lelem3  46630  hoidmv1le  46631  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  hoidmvlelem5  46636  hoidmvle  46637  ovnhoilem2  46639  ovnhoi  46640  hspmbllem2  46664  hspmbl  46666  hoimbl  46668  opnvonmbllem2  46670  ovnsubadd2  46683  ovolval4  46688  ovolval5lem3  46691  ovnovollem3  46695  iccvonmbl  46716  vonioolem2  46718  vonioo  46719  vonicclem2  46721  vonicc  46722  smflimlem4  46811  smfsuplem2  46849  smflimsuplem1  46857  smflimsuplem8  46864  smflimsup  46865  fundcmpsurbijinjpreimafv  47437  prproropf1o  47537  isuspgrim0  47924  cycldlenngric  47958  isubgr3stgrlem8  48003  rmsupp0  48398  domnmsuppn0  48399  rmsuppss  48400  suppmptcfin  48406  ply1mulgsum  48421  lcoc0  48453  linc1  48456  lcoel0  48459  lcoss  48467  el0ldep  48497  lincresunit3  48512  isldepslvec2  48516  itcovalpclem2  48702  itcovalt2lem2  48707  amgmlemALT  49834