Theorem cbvmptv 5190

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 5191 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 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2748	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 633	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5164	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5168	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5168	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2770	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5148   ↦ cmpt 5167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-opab 5149  df-mpt 5168

This theorem is referenced by:  fnmptfvd  6987  mptcnfimad  7932  onnseq  8277  rdgsucmpt2  8362  frsucmpt2  8372  fsetfocdm  8801  fsetprcnex  8802  resixpfo  8877  pw2f1olem  9012  xpmapen  9076  dffi3  9337  ordtypecbv  9425  inf3lema  9536  cantnflem1  9601  cnfcomlem  9611  infxpenc2  9935  fseqenlem1  9937  dfac8a  9943  dfac12r  10060  r1om  10156  fictb  10157  cfsmo  10184  coftr  10186  fin23lem38  10262  compsscnv  10284  isf34lem1  10285  compss  10289  fin1a2lem1  10313  fin1a2lem3  10315  fin1a2lem13  10325  itunisuc  10332  hsmex  10345  domtriom  10356  axdc2  10362  zorn2g  10416  ttukey2g  10429  axdc  10434  konigth  10483  pwcfsdom  10497  canthp1  10568  wunex2  10652  wuncval2  10661  negiso  12127  infrenegsup  12130  rpnnen1  12924  caurcvg2  15631  caucvg  15632  summo  15670  zsum  15671  fsum  15673  ackbijnn  15784  cbvprodv  15870  prodmo  15892  zprod  15893  fprod  15897  iprodmul  15959  bpolyval  16005  phimullem  16740  eulerth  16744  iserodd  16797  prmreclem5  16882  prmrec  16884  vdwlem7  16949  vdwlem9  16951  vdwlem10  16952  ramub1  16990  ramcl  16991  yonedalem4c  18234  yonedalem3b  18236  gsumwspan  18805  smndex1iidm  18860  smndex1gid  18863  smndex1gidOLD  18864  smndex2dlinvh  18879  grplactcnv  19010  gicqusker  19254  galactghm  19370  symgfixfo  19405  pmtrdifwrdel  19451  pmtrdifwrdel2  19452  odf1o2  19539  sylow1lem2  19565  sylow1  19569  sylow2b  19589  sylow3lem1  19593  sylow3lem5  19597  sylow3  19599  efgtf  19688  efgsval  19697  ghmcyg  19862  cycsubgcyg  19867  ablfaclem3  20055  ablfac2  20057  srgbinomlem4  20201  funcrngcsetcALT  20609  fidomndrnglem  20740  isphld  21644  frlmphl  21771  mplmonmul  22024  evlslem2  22067  mat1ric  22462  mdetralt  22583  smadiadetlem3  22643  pmatcollpw3lem  22758  mp2pm2mplem5  22785  mp2pm2mp  22786  pm2mpmhmlem2  22794  cpmidpmat  22848  cpmadugsumlemF  22851  cpmadugsumfi  22852  cpmadumatpoly  22858  chcoeffeqlem  22860  cayleyhamilton0  22864  cayleyhamilton  22865  cayleyhamiltonALT  22866  cayleyhamilton1  22867  ordtbaslem  23163  ordtbas2  23166  lly1stc  23471  ptpjopn  23587  xkohmeo  23790  fbasrn  23859  elfm  23922  tmdmulg  24067  tmdgsum  24070  qustgpopn  24095  tsmsfbas  24103  tsmsf1o  24120  ustuqtoplem  24214  utopsnneip  24223  fmucnd  24266  ucnextcn  24278  met1stc  24496  prdsxmslem2  24504  metustto  24528  metustexhalf  24531  metuust  24535  cfilucfil2  24536  metuel  24539  metuel2  24540  psmetutop  24542  restmetu  24545  metucn  24546  xrge0tsms  24810  metdsge  24825  expcn  24849  pi1xfrcnv  25034  minveclem3b  25405  minveclem5  25410  minvec  25413  ovollb2  25466  ovolshftlem2  25487  ovolscalem2  25491  ovolicc  25500  ioombl1  25539  uniioombllem6  25565  volsup2  25582  vitali  25590  mbfi1fseq  25698  mbfmullem  25702  itg2seq  25719  itg2i1fseq  25732  itg2addlem  25735  itg2cnlem1  25738  itg2cn  25740  cbvitgv  25754  dvfsumrlimge0  26007  plyadd  26192  plymul  26193  coeeu  26200  coeid  26213  dvply2g  26261  dvply2gOLD  26262  plydivex  26274  elqaalem2  26297  elqaa  26299  taylthlem1  26350  taylth  26353  pserval  26388  radcnvlem2  26392  radcnvlt2  26397  dvradcnv  26399  pserulm  26400  psercn  26404  pserdvlem2  26406  pserdv  26407  efgh  26518  eff1olem  26525  circgrp  26529  circsubm  26530  logno1  26613  emcl  26980  harmonicbnd  26981  harmonicbnd2  26982  basel  27067  musum  27168  dchr1  27234  dchrptlem2  27242  dchrpt  27244  lgsqrlem4  27326  lgseisenlem3  27354  2sqlem1  27394  dchrmusumlema  27470  dchrmusum2  27471  dchrvmasumlema  27477  dchrvmasumiflem1  27478  dchrisum0ff  27484  dchrisum0lema  27491  dchrisum0lem1b  27492  dchrisum0lem2a  27494  nosupcbv  27680  noinfcbv  27695  precsexlemcbv  28212  seqsfn  28315  seqsp1  28317  wlknwwlksnbij  29971  clwlkclwwlken  30097  clwlknf1oclwwlkn  30169  frgrncvvdeqlem8  30391  frgrncvvdeqlem9  30392  numclwwlk1lem2  30445  ubthlem3  30958  minveco  30970  htth  31004  fsuppcurry1  32812  fsuppcurry2  32813  gsumhashmul  33143  gsummulsubdishift1  33144  gsummulsubdishift1s  33146  gsummulsubdishift2s  33147  xrge0tsmsd  33149  elrgspnlem1  33318  elrgspnlem2  33319  elrgspn  33322  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrgspnsubrun  33325  idomsubr  33385  nsgmgc  33487  nsgqusf1olem1  33488  lmicqusker  33493  ricqusker  33502  elrspunidl  33503  elrspunsn  33504  zringfrac  33629  mplvrpmga  33704  mplvrpmrhm  33706  psrgsum  33707  psrmonmul  33709  psrmonprod  33711  splysubrg  33719  issply  33720  esplyfvaln  33733  vietalem  33738  vieta  33739  ply1degltdim  33783  lbsdiflsp0  33786  fedgmullem1  33789  fedgmul  33791  assarrginv  33796  evls1fldgencl  33830  fldextrspunlsplem  33833  fldextrspunlsp  33834  extdgfialglem2  33853  extdgfialg  33854  algextdeglem4  33880  algextdeg  33885  constrcbvlem  33915  madjusmdetlem2  33988  madjusmdet  33991  zartop  34036  zartopon  34037  zart0  34039  zarmxt1  34040  zarcmp  34042  rhmpreimacn  34045  xrge0mulc1cn  34101  xrge0tmd  34105  xrge0tmdALT  34106  cbvesumv  34203  gsumesum  34219  esumlub  34220  esumpcvgval  34238  esumcvg  34246  esumcvg2  34247  eulerpartlems  34520  eulerpart  34542  fibp1  34561  rrvadd  34612  ballotlemfval  34650  ballotlemi  34661  ballotlemsval  34669  ballotlemsv  34670  ballotlemsf1o  34674  ballotlemrval  34678  ballotlemrinv  34694  signsply0  34711  actfunsnf1o  34764  actfunsnrndisj  34765  itgexpif  34766  hgt750lemb  34816  onvf1odlem3  35303  derangfmla  35388  erdsze  35400  pconnpi1  35435  cvmscbv  35456  cvmsss2  35472  cvmliftlem15  35496  cvmlift2  35514  cvmlift3  35526  elmrsubrn  35718  iprodefisum  35939  cbvprodvw2  36445  cbvitgvw2  36446  knoppcnlem7  36775  knoppf  36811  f1omptsn  37667  mptsnun  37669  fin2so  37942  poimirlem27  37982  broucube  37989  ftc1anclem5  38032  ftc1anclem6  38033  sdclem2  38077  prdstotbnd  38129  prdsbnd2  38130  heiborlem10  38155  lshpkrcl  39576  tendoplcbv  41235  tendo0cbv  41246  tendoicbv  41253  lcfl7N  41961  lcf1o  42011  hdmap1cbv  42262  frlmsnic  42999  evlselv  43034  mzpclval  43171  mzpcompact2lem  43197  rmxyval  43361  dnnumch1  43490  aomclem3  43502  aomclem8  43507  dfac21  43512  pwfi2f1o  43542  dftrcl3  44165  dfrtrcl3  44178  rfovcnvf1od  44449  fsovrfovd  44454  fsovcnvlem  44458  dssmapnvod  44465  clsk3nimkb  44485  radcnvrat  44759  expgrowthi  44778  expgrowth  44780  dvradcnv2  44792  binomcxplemradcnv  44797  binomcxplemdvbinom  44798  binomcxplemdvsum  44800  binomcxplemnotnn0  44801  binomcxp  44802  wessf1ornlem  45633  projf1o  45644  fsumsermpt  46027  fmuldfeqlem1  46030  fprodcn  46048  sumnnodd  46078  limsupvaluz  46154  limsupvaluz2  46184  supcnvlimsup  46186  supcnvlimsupmpt  46187  liminfval2  46214  liminflelimsuplem  46221  fprodsubrecnncnv  46354  fprodaddrecnncnv  46356  dvsinax  46359  fperdvper  46365  dvcosax  46372  ioodvbdlimc1lem1  46377  ioodvbdlimc1  46379  ioodvbdlimc2  46381  dvnmul  46389  dvnprodlem1  46392  dvnprodlem2  46393  dvnprodlem3  46394  dvnprod  46395  itgsin0pilem1  46396  itgiccshift  46426  stoweidlem2  46448  stoweidlem17  46463  stoweidlem32  46478  stoweidlem34  46480  stoweidlem43  46489  stirlinglem2  46521  stirlinglem3  46522  stirlinglem8  46527  dirkerval  46537  dirkerval2  46540  dirkeritg  46548  dirkercncflem3  46551  dirkercncf  46553  fourierdlem14  46567  fourierdlem18  46571  fourierdlem53  46605  fourierdlem62  46614  fourierdlem71  46623  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem80  46632  fourierdlem81  46633  fourierdlem84  46636  fourierdlem88  46640  fourierdlem92  46644  fourierdlem93  46645  fourierdlem94  46646  fourierdlem95  46647  fourierdlem96  46648  fourierdlem97  46649  fourierdlem98  46650  fourierdlem99  46651  fourierdlem101  46653  fourierdlem103  46655  fourierdlem104  46656  fourierdlem105  46657  fourierdlem106  46658  fourierdlem107  46659  fourierdlem108  46660  fourierdlem110  46662  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  fourierdlem115  46667  fouriersw  46677  elaa2  46680  etransclem1  46681  etransclem5  46685  etransclem6  46686  etransclem11  46691  etransclem13  46693  etransclem41  46721  etransclem47  46727  etransc  46729  ioorrnopn  46751  ioorrnopnxr  46753  subsaliuncl  46804  sge0resplit  46852  sge0fodjrnlem  46862  nnfoctbdj  46902  iundjiun  46906  voliunsge0lem  46918  meaiuninclem  46926  meaiuninc  46927  meaiininclem  46932  meaiininc  46933  omeiunltfirp  46965  carageniuncllem2  46968  carageniuncl  46969  0ome  46975  isomennd  46977  hoicvrrex  47002  ovn0  47012  ovnsubaddlem2  47017  ovnsubadd  47018  sge0hsphoire  47035  hoidmv1lelem3  47039  hoidmv1le  47040  hoidmvlelem1  47041  hoidmvlelem2  47042  hoidmvlelem3  47043  hoidmvlelem4  47044  hoidmvlelem5  47045  hoidmvle  47046  ovnhoilem2  47048  ovnhoi  47049  hspmbllem2  47073  hspmbl  47075  hoimbl  47077  opnvonmbllem2  47079  ovnsubadd2  47092  ovolval4  47097  ovolval5lem3  47100  ovnovollem3  47104  iccvonmbl  47125  vonioolem2  47127  vonioo  47128  vonicclem2  47130  vonicc  47131  smflimlem4  47220  smfsuplem2  47258  smflimsuplem1  47266  smflimsuplem8  47273  smflimsup  47274  fundcmpsurbijinjpreimafv  47879  prproropf1o  47979  isuspgrim0  48382  cycldlenngric  48416  isubgr3stgrlem8  48461  rmsupp0  48856  domnmsuppn0  48857  rmsuppss  48858  suppmptcfin  48864  ply1mulgsum  48878  lcoc0  48910  linc1  48913  lcoel0  48916  lcoss  48924  el0ldep  48954  lincresunit3  48969  isldepslvec2  48973  itcovalpclem2  49159  itcovalt2lem2  49164  amgmlemALT  50290