Theorem cbvmptv 5202

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 5203 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 2819	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2747	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5176	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5180	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5180	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2769	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {copab 5160   ↦ cmpt 5179

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-opab 5161  df-mpt 5180

This theorem is referenced by:  fnmptfvd  6986  mptcnfimad  7930  onnseq  8276  rdgsucmpt2  8361  frsucmpt2  8371  fsetfocdm  8798  fsetprcnex  8799  resixpfo  8874  pw2f1olem  9009  xpmapen  9073  dffi3  9334  ordtypecbv  9422  inf3lema  9533  cantnflem1  9598  cnfcomlem  9608  infxpenc2  9932  fseqenlem1  9934  dfac8a  9940  dfac12r  10057  r1om  10153  fictb  10154  cfsmo  10181  coftr  10183  fin23lem38  10259  compsscnv  10281  isf34lem1  10282  compss  10286  fin1a2lem1  10310  fin1a2lem3  10312  fin1a2lem13  10322  itunisuc  10329  hsmex  10342  domtriom  10353  axdc2  10359  zorn2g  10413  ttukey2g  10426  axdc  10431  konigth  10480  pwcfsdom  10494  canthp1  10565  wunex2  10649  wuncval2  10658  negiso  12122  infrenegsup  12125  rpnnen1  12896  caurcvg2  15601  caucvg  15602  summo  15640  zsum  15641  fsum  15643  ackbijnn  15751  cbvprodv  15837  prodmo  15859  zprod  15860  fprod  15864  iprodmul  15926  bpolyval  15972  phimullem  16706  eulerth  16710  iserodd  16763  prmreclem5  16848  prmrec  16850  vdwlem7  16915  vdwlem9  16917  vdwlem10  16918  ramub1  16956  ramcl  16957  yonedalem4c  18200  yonedalem3b  18202  gsumwspan  18771  smndex1iidm  18826  smndex1gid  18828  smndex2dlinvh  18842  grplactcnv  18973  gicqusker  19217  galactghm  19333  symgfixfo  19368  pmtrdifwrdel  19414  pmtrdifwrdel2  19415  odf1o2  19502  sylow1lem2  19528  sylow1  19532  sylow2b  19552  sylow3lem1  19556  sylow3lem5  19560  sylow3  19562  efgtf  19651  efgsval  19660  ghmcyg  19825  cycsubgcyg  19830  ablfaclem3  20018  ablfac2  20020  srgbinomlem4  20164  funcrngcsetcALT  20574  fidomndrnglem  20705  isphld  21609  frlmphl  21736  mplmonmul  21991  evlslem2  22034  mat1ric  22431  mdetralt  22552  smadiadetlem3  22612  pmatcollpw3lem  22727  mp2pm2mplem5  22754  mp2pm2mp  22755  pm2mpmhmlem2  22763  cpmidpmat  22817  cpmadugsumlemF  22820  cpmadugsumfi  22821  cpmadumatpoly  22827  chcoeffeqlem  22829  cayleyhamilton0  22833  cayleyhamilton  22834  cayleyhamiltonALT  22835  cayleyhamilton1  22836  ordtbaslem  23132  ordtbas2  23135  lly1stc  23440  ptpjopn  23556  xkohmeo  23759  fbasrn  23828  elfm  23891  tmdmulg  24036  tmdgsum  24039  qustgpopn  24064  tsmsfbas  24072  tsmsf1o  24089  ustuqtoplem  24183  utopsnneip  24192  fmucnd  24235  ucnextcn  24247  met1stc  24465  prdsxmslem2  24473  metustto  24497  metustexhalf  24500  metuust  24504  cfilucfil2  24505  metuel  24508  metuel2  24509  psmetutop  24511  restmetu  24514  metucn  24515  xrge0tsms  24779  metdsge  24794  expcn  24819  expcnOLD  24821  pi1xfrcnv  25013  minveclem3b  25384  minveclem5  25389  minvec  25392  ovollb2  25446  ovolshftlem2  25467  ovolscalem2  25471  ovolicc  25480  ioombl1  25519  uniioombllem6  25545  volsup2  25562  vitali  25570  mbfi1fseq  25678  mbfmullem  25682  itg2seq  25699  itg2i1fseq  25712  itg2addlem  25715  itg2cnlem1  25718  itg2cn  25720  cbvitgv  25734  dvfsumrlimge0  25993  plyadd  26178  plymul  26179  coeeu  26186  coeid  26199  dvply2g  26248  dvply2gOLD  26249  plydivex  26261  elqaalem2  26284  elqaa  26286  taylthlem1  26337  taylth  26340  pserval  26375  radcnvlem2  26379  radcnvlt2  26384  dvradcnv  26386  pserulm  26387  psercn  26392  pserdvlem2  26394  pserdv  26395  efgh  26506  eff1olem  26513  circgrp  26517  circsubm  26518  logno1  26601  emcl  26969  harmonicbnd  26970  harmonicbnd2  26971  basel  27056  musum  27157  dchr1  27224  dchrptlem2  27232  dchrpt  27234  lgsqrlem4  27316  lgseisenlem3  27344  2sqlem1  27384  dchrmusumlema  27460  dchrmusum2  27461  dchrvmasumlema  27467  dchrvmasumiflem1  27468  dchrisum0ff  27474  dchrisum0lema  27481  dchrisum0lem1b  27482  dchrisum0lem2a  27484  nosupcbv  27670  noinfcbv  27685  precsexlemcbv  28202  seqsfn  28305  seqsp1  28307  wlknwwlksnbij  29961  clwlkclwwlken  30087  clwlknf1oclwwlkn  30159  frgrncvvdeqlem8  30381  frgrncvvdeqlem9  30382  numclwwlk1lem2  30435  ubthlem3  30947  minveco  30959  htth  30993  fsuppcurry1  32803  fsuppcurry2  32804  gsumhashmul  33150  gsummulsubdishift1  33151  gsummulsubdishift1s  33153  gsummulsubdishift2s  33154  xrge0tsmsd  33155  elrgspnlem1  33324  elrgspnlem2  33325  elrgspn  33328  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrgspnsubrun  33331  idomsubr  33391  nsgmgc  33493  nsgqusf1olem1  33494  lmicqusker  33499  ricqusker  33508  elrspunidl  33509  elrspunsn  33510  zringfrac  33635  mplvrpmga  33710  mplvrpmrhm  33712  splysubrg  33718  issply  33719  vietalem  33735  vieta  33736  ply1degltdim  33780  lbsdiflsp0  33783  fedgmullem1  33786  fedgmul  33788  assarrginv  33793  evls1fldgencl  33827  fldextrspunlsplem  33830  fldextrspunlsp  33831  extdgfialglem2  33850  extdgfialg  33851  algextdeglem4  33877  algextdeg  33882  constrcbvlem  33912  madjusmdetlem2  33985  madjusmdet  33988  zartop  34033  zartopon  34034  zart0  34036  zarmxt1  34037  zarcmp  34039  rhmpreimacn  34042  xrge0mulc1cn  34098  xrge0tmd  34102  xrge0tmdALT  34103  cbvesumv  34200  gsumesum  34216  esumlub  34217  esumpcvgval  34235  esumcvg  34243  esumcvg2  34244  eulerpartlems  34517  eulerpart  34539  fibp1  34558  rrvadd  34609  ballotlemfval  34647  ballotlemi  34658  ballotlemsval  34666  ballotlemsv  34667  ballotlemsf1o  34671  ballotlemrval  34675  ballotlemrinv  34691  signsply0  34708  actfunsnf1o  34761  actfunsnrndisj  34762  itgexpif  34763  hgt750lemb  34813  onvf1odlem3  35299  derangfmla  35384  erdsze  35396  pconnpi1  35431  cvmscbv  35452  cvmsss2  35468  cvmliftlem15  35492  cvmlift2  35510  cvmlift3  35522  elmrsubrn  35714  iprodefisum  35935  cbvprodvw2  36441  cbvitgvw2  36442  knoppcnlem7  36699  knoppf  36735  f1omptsn  37538  mptsnun  37540  fin2so  37804  poimirlem27  37844  broucube  37851  ftc1anclem5  37894  ftc1anclem6  37895  sdclem2  37939  prdstotbnd  37991  prdsbnd2  37992  heiborlem10  38017  lshpkrcl  39372  tendoplcbv  41031  tendo0cbv  41042  tendoicbv  41049  lcfl7N  41757  lcf1o  41807  hdmap1cbv  42058  frlmsnic  42791  evlselv  42826  mzpclval  42963  mzpcompact2lem  42989  rmxyval  43153  dnnumch1  43282  aomclem3  43294  aomclem8  43299  dfac21  43304  pwfi2f1o  43334  dftrcl3  43957  dfrtrcl3  43970  rfovcnvf1od  44241  fsovrfovd  44246  fsovcnvlem  44250  dssmapnvod  44257  clsk3nimkb  44277  radcnvrat  44551  expgrowthi  44570  expgrowth  44572  dvradcnv2  44584  binomcxplemradcnv  44589  binomcxplemdvbinom  44590  binomcxplemdvsum  44592  binomcxplemnotnn0  44593  binomcxp  44594  wessf1ornlem  45425  projf1o  45437  fsumsermpt  45821  fmuldfeqlem1  45824  fprodcn  45842  sumnnodd  45872  limsupvaluz  45948  limsupvaluz2  45978  supcnvlimsup  45980  supcnvlimsupmpt  45981  liminfval2  46008  liminflelimsuplem  46015  fprodsubrecnncnv  46148  fprodaddrecnncnv  46150  dvsinax  46153  fperdvper  46159  dvcosax  46166  ioodvbdlimc1lem1  46171  ioodvbdlimc1  46173  ioodvbdlimc2  46175  dvnmul  46183  dvnprodlem1  46186  dvnprodlem2  46187  dvnprodlem3  46188  dvnprod  46189  itgsin0pilem1  46190  itgiccshift  46220  stoweidlem2  46242  stoweidlem17  46257  stoweidlem32  46272  stoweidlem34  46274  stoweidlem43  46283  stirlinglem2  46315  stirlinglem3  46316  stirlinglem8  46321  dirkerval  46331  dirkerval2  46334  dirkeritg  46342  dirkercncflem3  46345  dirkercncf  46347  fourierdlem14  46361  fourierdlem18  46365  fourierdlem53  46399  fourierdlem62  46408  fourierdlem71  46417  fourierdlem74  46420  fourierdlem75  46421  fourierdlem76  46422  fourierdlem80  46426  fourierdlem81  46427  fourierdlem84  46430  fourierdlem88  46434  fourierdlem92  46438  fourierdlem93  46439  fourierdlem94  46440  fourierdlem95  46441  fourierdlem96  46442  fourierdlem97  46443  fourierdlem98  46444  fourierdlem99  46445  fourierdlem101  46447  fourierdlem103  46449  fourierdlem104  46450  fourierdlem105  46451  fourierdlem106  46452  fourierdlem107  46453  fourierdlem108  46454  fourierdlem110  46456  fourierdlem111  46457  fourierdlem112  46458  fourierdlem113  46459  fourierdlem115  46461  fouriersw  46471  elaa2  46474  etransclem1  46475  etransclem5  46479  etransclem6  46480  etransclem11  46485  etransclem13  46487  etransclem41  46515  etransclem47  46521  etransc  46523  ioorrnopn  46545  ioorrnopnxr  46547  subsaliuncl  46598  sge0resplit  46646  sge0fodjrnlem  46656  nnfoctbdj  46696  iundjiun  46700  voliunsge0lem  46712  meaiuninclem  46720  meaiuninc  46721  meaiininclem  46726  meaiininc  46727  omeiunltfirp  46759  carageniuncllem2  46762  carageniuncl  46763  0ome  46769  isomennd  46771  hoicvrrex  46796  ovn0  46806  ovnsubaddlem2  46811  ovnsubadd  46812  sge0hsphoire  46829  hoidmv1lelem3  46833  hoidmv1le  46834  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  hoidmvlelem5  46839  hoidmvle  46840  ovnhoilem2  46842  ovnhoi  46843  hspmbllem2  46867  hspmbl  46869  hoimbl  46871  opnvonmbllem2  46873  ovnsubadd2  46886  ovolval4  46891  ovolval5lem3  46894  ovnovollem3  46898  iccvonmbl  46919  vonioolem2  46921  vonioo  46922  vonicclem2  46924  vonicc  46925  smflimlem4  47014  smfsuplem2  47052  smflimsuplem1  47060  smflimsuplem8  47067  smflimsup  47068  fundcmpsurbijinjpreimafv  47649  prproropf1o  47749  isuspgrim0  48136  cycldlenngric  48170  isubgr3stgrlem8  48215  rmsupp0  48610  domnmsuppn0  48611  rmsuppss  48612  suppmptcfin  48618  ply1mulgsum  48632  lcoc0  48664  linc1  48667  lcoel0  48670  lcoss  48678  el0ldep  48708  lincresunit3  48723  isldepslvec2  48727  itcovalpclem2  48913  itcovalt2lem2  48918  amgmlemALT  50044