Theorem cbvmptv 5225

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 5227 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 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2746	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5197	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5202	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5202	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2768	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {copab 5181   ↦ cmpt 5201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-mpt 5202

This theorem is referenced by:  fnmptfvd  7030  mptcnfimad  7983  onnseq  8356  rdgsucmpt2  8442  frsucmpt2  8452  fsetfocdm  8873  fsetprcnex  8874  resixpfo  8948  pw2f1olem  9088  xpmapen  9157  dffi3  9441  ordtypecbv  9529  inf3lema  9636  cantnflem1  9701  cnfcomlem  9711  infxpenc2  10034  fseqenlem1  10036  dfac8a  10042  dfac12r  10159  r1om  10255  fictb  10256  cfsmo  10283  coftr  10285  fin23lem38  10361  compsscnv  10383  isf34lem1  10384  compss  10388  fin1a2lem1  10412  fin1a2lem3  10414  fin1a2lem13  10424  itunisuc  10431  hsmex  10444  domtriom  10455  axdc2  10461  zorn2g  10515  ttukey2g  10528  axdc  10533  konigth  10581  pwcfsdom  10595  canthp1  10666  wunex2  10750  wuncval2  10759  negiso  12220  infrenegsup  12223  rpnnen1  12997  caurcvg2  15692  caucvg  15693  summo  15731  zsum  15732  fsum  15734  ackbijnn  15842  cbvprodv  15928  prodmo  15950  zprod  15951  fprod  15955  iprodmul  16017  bpolyval  16063  phimullem  16796  eulerth  16800  iserodd  16853  prmreclem5  16938  prmrec  16940  vdwlem7  17005  vdwlem9  17007  vdwlem10  17008  ramub1  17046  ramcl  17047  yonedalem4c  18287  yonedalem3b  18289  gsumwspan  18822  smndex1iidm  18877  smndex1gid  18879  smndex2dlinvh  18893  grplactcnv  19024  gicqusker  19269  galactghm  19383  symgfixfo  19418  pmtrdifwrdel  19464  pmtrdifwrdel2  19465  odf1o2  19552  sylow1lem2  19578  sylow1  19582  sylow2b  19602  sylow3lem1  19606  sylow3lem5  19610  sylow3  19612  efgtf  19701  efgsval  19710  ghmcyg  19875  cycsubgcyg  19880  ablfaclem3  20068  ablfac2  20070  srgbinomlem4  20187  funcrngcsetcALT  20599  fidomndrnglem  20730  isphld  21612  frlmphl  21739  mplmonmul  21992  evlslem2  22035  mat1ric  22423  mdetralt  22544  smadiadetlem3  22604  pmatcollpw3lem  22719  mp2pm2mplem5  22746  mp2pm2mp  22747  pm2mpmhmlem2  22755  cpmidpmat  22809  cpmadugsumlemF  22812  cpmadugsumfi  22813  cpmadumatpoly  22819  chcoeffeqlem  22821  cayleyhamilton0  22825  cayleyhamilton  22826  cayleyhamiltonALT  22827  cayleyhamilton1  22828  ordtbaslem  23124  ordtbas2  23127  lly1stc  23432  ptpjopn  23548  xkohmeo  23751  fbasrn  23820  elfm  23883  tmdmulg  24028  tmdgsum  24031  qustgpopn  24056  tsmsfbas  24064  tsmsf1o  24081  ustuqtoplem  24176  utopsnneip  24185  fmucnd  24228  ucnextcn  24240  met1stc  24458  prdsxmslem2  24466  metustto  24490  metustexhalf  24493  metuust  24497  cfilucfil2  24498  metuel  24501  metuel2  24502  psmetutop  24504  restmetu  24507  metucn  24508  xrge0tsms  24772  metdsge  24787  expcn  24812  expcnOLD  24814  pi1xfrcnv  25006  minveclem3b  25378  minveclem5  25383  minvec  25386  ovollb2  25440  ovolshftlem2  25461  ovolscalem2  25465  ovolicc  25474  ioombl1  25513  uniioombllem6  25539  volsup2  25556  vitali  25564  mbfi1fseq  25672  mbfmullem  25676  itg2seq  25693  itg2i1fseq  25706  itg2addlem  25709  itg2cnlem1  25712  itg2cn  25714  cbvitgv  25728  dvfsumrlimge0  25987  plyadd  26172  plymul  26173  coeeu  26180  coeid  26193  dvply2g  26242  dvply2gOLD  26243  plydivex  26255  elqaalem2  26278  elqaa  26280  taylthlem1  26331  taylth  26334  pserval  26369  radcnvlem2  26373  radcnvlt2  26378  dvradcnv  26380  pserulm  26381  psercn  26386  pserdvlem2  26388  pserdv  26389  efgh  26500  eff1olem  26507  circgrp  26511  circsubm  26512  logno1  26595  emcl  26963  harmonicbnd  26964  harmonicbnd2  26965  basel  27050  musum  27151  dchr1  27218  dchrptlem2  27226  dchrpt  27228  lgsqrlem4  27310  lgseisenlem3  27338  2sqlem1  27378  dchrmusumlema  27454  dchrmusum2  27455  dchrvmasumlema  27461  dchrvmasumiflem1  27462  dchrisum0ff  27468  dchrisum0lema  27475  dchrisum0lem1b  27476  dchrisum0lem2a  27478  nosupcbv  27664  noinfcbv  27679  precsexlemcbv  28147  seqsfn  28232  seqsp1  28234  wlknwwlksnbij  29816  clwlkclwwlken  29939  clwlknf1oclwwlkn  30011  frgrncvvdeqlem8  30233  frgrncvvdeqlem9  30234  numclwwlk1lem2  30287  ubthlem3  30799  minveco  30811  htth  30845  fsuppcurry1  32648  fsuppcurry2  32649  gsumhashmul  33001  xrge0tsmsd  33002  elrgspnlem1  33183  elrgspnlem2  33184  elrgspn  33187  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  elrgspnsubrun  33190  idomsubr  33249  nsgmgc  33373  nsgqusf1olem1  33374  lmicqusker  33379  ricqusker  33388  elrspunidl  33389  elrspunsn  33390  zringfrac  33515  ply1degltdim  33609  lbsdiflsp0  33612  fedgmullem1  33615  fedgmul  33617  assarrginv  33622  evls1fldgencl  33657  fldextrspunlsplem  33660  fldextrspunlsp  33661  algextdeglem4  33700  algextdeg  33705  constrcbvlem  33735  madjusmdetlem2  33805  madjusmdet  33808  zartop  33853  zartopon  33854  zart0  33856  zarmxt1  33857  zarcmp  33859  rhmpreimacn  33862  xrge0mulc1cn  33918  xrge0tmd  33922  xrge0tmdALT  33923  cbvesumv  34020  gsumesum  34036  esumlub  34037  esumpcvgval  34055  esumcvg  34063  esumcvg2  34064  eulerpartlems  34338  eulerpart  34360  fibp1  34379  rrvadd  34430  ballotlemfval  34468  ballotlemi  34479  ballotlemsval  34487  ballotlemsv  34488  ballotlemsf1o  34492  ballotlemrval  34496  ballotlemrinv  34512  signsply0  34529  actfunsnf1o  34582  actfunsnrndisj  34583  itgexpif  34584  hgt750lemb  34634  derangfmla  35158  erdsze  35170  pconnpi1  35205  cvmscbv  35226  cvmsss2  35242  cvmliftlem15  35266  cvmlift2  35284  cvmlift3  35296  elmrsubrn  35488  iprodefisum  35704  cbvprodvw2  36211  cbvitgvw2  36212  knoppcnlem7  36463  knoppf  36499  f1omptsn  37301  mptsnun  37303  fin2so  37577  poimirlem27  37617  broucube  37624  ftc1anclem5  37667  ftc1anclem6  37668  sdclem2  37712  prdstotbnd  37764  prdsbnd2  37765  heiborlem10  37790  lshpkrcl  39080  tendoplcbv  40740  tendo0cbv  40751  tendoicbv  40758  lcfl7N  41466  lcf1o  41516  hdmap1cbv  41767  frlmsnic  42510  evlselv  42557  mzpclval  42695  mzpcompact2lem  42721  rmxyval  42886  dnnumch1  43015  aomclem3  43027  aomclem8  43032  dfac21  43037  pwfi2f1o  43067  dftrcl3  43691  dfrtrcl3  43704  rfovcnvf1od  43975  fsovrfovd  43980  fsovcnvlem  43984  dssmapnvod  43991  clsk3nimkb  44011  radcnvrat  44286  expgrowthi  44305  expgrowth  44307  dvradcnv2  44319  binomcxplemradcnv  44324  binomcxplemdvbinom  44325  binomcxplemdvsum  44327  binomcxplemnotnn0  44328  binomcxp  44329  wessf1ornlem  45157  projf1o  45169  fsumsermpt  45556  fmuldfeqlem1  45559  fprodcn  45577  sumnnodd  45607  limsupvaluz  45685  limsupvaluz2  45715  supcnvlimsup  45717  supcnvlimsupmpt  45718  liminfval2  45745  liminflelimsuplem  45752  fprodsubrecnncnv  45885  fprodaddrecnncnv  45887  dvsinax  45890  fperdvper  45896  dvcosax  45903  ioodvbdlimc1lem1  45908  ioodvbdlimc1  45910  ioodvbdlimc2  45912  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  dvnprodlem3  45925  dvnprod  45926  itgsin0pilem1  45927  itgiccshift  45957  stoweidlem2  45979  stoweidlem17  45994  stoweidlem32  46009  stoweidlem34  46011  stoweidlem43  46020  stirlinglem2  46052  stirlinglem3  46053  stirlinglem8  46058  dirkerval  46068  dirkerval2  46071  dirkeritg  46079  dirkercncflem3  46082  dirkercncf  46084  fourierdlem14  46098  fourierdlem18  46102  fourierdlem53  46136  fourierdlem62  46145  fourierdlem71  46154  fourierdlem74  46157  fourierdlem75  46158  fourierdlem76  46159  fourierdlem80  46163  fourierdlem81  46164  fourierdlem84  46167  fourierdlem88  46171  fourierdlem92  46175  fourierdlem93  46176  fourierdlem94  46177  fourierdlem95  46178  fourierdlem96  46179  fourierdlem97  46180  fourierdlem98  46181  fourierdlem99  46182  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem105  46188  fourierdlem106  46189  fourierdlem107  46190  fourierdlem108  46191  fourierdlem110  46193  fourierdlem111  46194  fourierdlem112  46195  fourierdlem113  46196  fourierdlem115  46198  fouriersw  46208  elaa2  46211  etransclem1  46212  etransclem5  46216  etransclem6  46217  etransclem11  46222  etransclem13  46224  etransclem41  46252  etransclem47  46258  etransc  46260  ioorrnopn  46282  ioorrnopnxr  46284  subsaliuncl  46335  sge0resplit  46383  sge0fodjrnlem  46393  nnfoctbdj  46433  iundjiun  46437  voliunsge0lem  46449  meaiuninclem  46457  meaiuninc  46458  meaiininclem  46463  meaiininc  46464  omeiunltfirp  46496  carageniuncllem2  46499  carageniuncl  46500  0ome  46506  isomennd  46508  hoicvrrex  46533  ovn0  46543  ovnsubaddlem2  46548  ovnsubadd  46549  sge0hsphoire  46566  hoidmv1lelem3  46570  hoidmv1le  46571  hoidmvlelem1  46572  hoidmvlelem2  46573  hoidmvlelem3  46574  hoidmvlelem4  46575  hoidmvlelem5  46576  hoidmvle  46577  ovnhoilem2  46579  ovnhoi  46580  hspmbllem2  46604  hspmbl  46606  hoimbl  46608  opnvonmbllem2  46610  ovnsubadd2  46623  ovolval4  46628  ovolval5lem3  46631  ovnovollem3  46635  iccvonmbl  46656  vonioolem2  46658  vonioo  46659  vonicclem2  46661  vonicc  46662  smflimlem4  46751  smfsuplem2  46789  smflimsuplem1  46797  smflimsuplem8  46804  smflimsup  46805  fundcmpsurbijinjpreimafv  47369  prproropf1o  47469  isuspgrim0  47855  cycldlenngric  47889  isubgr3stgrlem8  47933  rmsupp0  48291  domnmsuppn0  48292  rmsuppss  48293  suppmptcfin  48299  ply1mulgsum  48314  lcoc0  48346  linc1  48349  lcoel0  48352  lcoss  48360  el0ldep  48390  lincresunit3  48405  isldepslvec2  48409  itcovalpclem2  48599  itcovalt2lem2  48604  amgmlemALT  49615