Theorem cbvmptv 5213

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 5214 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 2845	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2773	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5187	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5191	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5191	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2795	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  {copab 5171   ↦ cmpt 5190

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-opab 5172  df-mpt 5191

This theorem is used by:  fnmptfvd  7037  mptcnfimad  7987  onnseq  8337  rdgsucmpt2  8423  frsucmpt2  8433  fsetfocdm  8866  fsetprcnex  8867  resixpfo  8947  pw2f1olem  9083  xpmapen  9147  dffi3  9405  ordtypecbv  9493  inf3lema  9607  cantnflem1  9672  cnfcomlem  9682  infxpenc2  10029  fseqenlem1  10031  dfac8a  10037  dfac12r  10153  r1om  10249  fictb  10250  cfsmo  10277  coftr  10279  fin23lem38  10355  compsscnv  10377  isf34lem1  10378  compss  10382  fin1a2lem1  10406  fin1a2lem3  10408  fin1a2lem13  10418  itunisuc  10425  hsmex  10438  domtriom  10449  axdc2  10455  zorn2g  10509  ttukey2g  10522  axdc  10527  konigth  10582  pwcfsdom  10596  canthp1  10667  wunex2  10751  wuncval2  10760  negiso  12223  infrenegsup  12226  rpnnen1  13037  caurcvg2  15769  caucvg  15770  summo  15807  zsum  15808  fsum  15810  ackbijnn  15921  cbvprodv  16007  prodmo  16029  zprod  16030  fprod  16034  iprodmul  16096  bpolyval  16141  phimullem  16876  eulerth  16880  iserodd  16933  prmreclem5  17018  prmrec  17020  vdwlem7  17085  vdwlem9  17087  vdwlem10  17088  ramub1  17126  ramcl  17127  yonedalem4c  18371  yonedalem3b  18373  gsumwspan  18961  smndex1iidm  19016  smndex1gid  19019  smndex1gidOLD  19020  smndex2dlinvh  19035  grplactcnv  19172  gicqusker  19421  galactghm  19537  symgfixfo  19572  pmtrdifwrdel  19618  pmtrdifwrdel2  19619  odf1o2  19706  sylow1lem2  19732  sylow1  19736  sylow2b  19756  sylow3lem1  19760  sylow3lem5  19764  sylow3  19766  efgtf  19855  efgsval  19864  ghmcyg  20029  cycsubgcyg  20034  ablfaclem3  20222  ablfac2  20224  srgbinomlem4  20374  funcrngcsetcALT  20809  fidomndrnglem  20945  isphld  21873  frlmphl  22000  mplmonmul  22258  evlslem2  22301  mat1ric  22715  mdetralt  22836  smadiadetlem3  22896  pmatcollpw3lem  23014  mp2pm2mplem5  23041  mp2pm2mp  23042  pm2mpmhmlem2  23050  cpmidpmat  23104  cpmadugsumlemF  23107  cpmadugsumfi  23108  cpmadumatpoly  23114  chcoeffeqlem  23116  cayleyhamilton0  23120  cayleyhamilton  23121  cayleyhamiltonALT  23122  cayleyhamilton1  23123  ordtbaslem  23419  ordtbas2  23422  lly1stc  23728  ptpjopn  23844  xkohmeo  24047  fbasrn  24116  elfm  24179  tmdmulg  24324  tmdgsum  24327  qustgpopn  24352  tsmsfbas  24360  tsmsf1o  24377  ustuqtoplem  24471  utopsnneip  24480  fmucnd  24523  ucnextcn  24535  met1stc  24753  prdsxmslem2  24761  metustto  24785  metustexhalf  24788  metuust  24792  cfilucfil2  24793  metuel  24796  metuel2  24797  psmetutop  24799  restmetu  24802  metucn  24803  xrge0tsms  25067  metdsge  25082  expcn  25106  pi1xfrcnv  25291  minveclem3b  25662  minveclem5  25667  minvec  25670  ovollb2  25723  ovolshftlem2  25744  ovolscalem2  25748  ovolicc  25757  ioombl1  25796  uniioombllem6  25822  volsup2  25839  vitali  25847  mbfi1fseq  25955  mbfmullem  25959  itg2seq  25976  itg2i1fseq  25989  itg2addlem  25992  itg2cnlem1  25995  itg2cn  25997  cbvitgv  26011  dvfsumrlimge0  26264  plyadd  26450  plymul  26451  coeeu  26458  coeid  26471  dvply2g  26522  plydivex  26534  elqaalem2  26559  elqaa  26561  taylthlem1  26616  taylth  26618  pserval  26653  radcnvlem2  26657  radcnvlt2  26662  dvradcnv  26664  pserulm  26665  psercn  26669  pserdvlem2  26671  pserdv  26672  efgh  26786  eff1olem  26793  circgrp  26797  circsubm  26798  logno1  26881  emcl  27247  harmonicbnd  27248  harmonicbnd2  27249  basel  27334  musum  27435  dchr1  27501  dchrptlem2  27509  dchrpt  27511  lgsqrlem4  27593  lgseisenlem3  27621  2sqlem1  27661  dchrmusumlema  27737  dchrmusum2  27738  dchrvmasumlema  27744  dchrvmasumiflem1  27745  dchrisum0ff  27751  dchrisum0lema  27758  dchrisum0lem1b  27759  dchrisum0lem2a  27761  nosupcbv  27946  noinfcbv  27961  precsexlemcbv  28479  seqsfn  28582  seqsp1  28584  wlknwwlksnbij  30364  clwlkclwwlken  30490  clwlknf1oclwwlkn  30562  frgrncvvdeqlem8  30794  frgrncvvdeqlem9  30795  numclwwlk1lem2  30848  ubthlem3  31361  minveco  31373  htth  31407  fsuppcurry1  33203  fsuppcurry2  33204  gsumhashmul  33515  gsummulsubdishift1  33516  gsummulsubdishift1s  33518  gsummulsubdishift2s  33519  xrge0tsmsd  33521  elrgspnlem1  33690  elrgspnlem2  33691  elrgspn  33694  elrgspnsubrunlem1  33695  elrgspnsubrunlem2  33696  elrgspnsubrun  33697  idomsubr  33758  nsgmgc  33849  nsgqusf1olem1  33850  lmicqusker  33855  ricqusker  33863  elrspunidl  33864  elrspunsn  33865  zringfrac  33972  0mplric  34033  selvply1rhmlemb  34037  selvply1rhmlem3  34040  selvply1rhmlem5  34042  selvply1rhm  34043  mplidom  34046  mplvrpmga  34063  mplvrpmrhm  34065  psrgsum  34066  psrmonmul  34068  psrmonprod  34070  splysubrg  34078  issply  34079  esplyfvaln  34092  vietalem  34097  vieta  34098  ply1degltdim  34141  lbsdiflsp0  34144  fedgmullem1  34147  fedgmul  34149  assarrginv  34154  evls1fldgencl  34188  fldextrspunlsplem  34191  fldextrspunlsp  34192  extdgfialglem2  34211  extdgfialg  34212  algextdeglem4  34238  algextdeg  34243  constrcbvlem  34273  madjusmdetlem2  34346  madjusmdet  34349  zartop  34394  zartopon  34395  zart0  34397  zarmxt1  34398  zarcmp  34400  rhmpreimacn  34403  xrge0mulc1cn  34459  xrge0tmd  34463  xrge0tmdALT  34464  cbvesumv  34561  gsumesum  34577  esumlub  34578  esumpcvgval  34596  esumcvg  34604  esumcvg2  34605  eulerpartlems  34879  eulerpart  34901  fibp1  34920  rrvadd  34971  ballotlemfval  35009  ballotlemi  35020  ballotlemsval  35028  ballotlemsv  35029  ballotlemsf1o  35033  ballotlemrval  35037  ballotlemrinv  35053  signsply0  35067  actfunsnf1o  35120  actfunsnrndisj  35121  itgexpif  35122  hgt750lemb  35172  onvf1odlem3  35710  derangfmla  35777  erdsze  35789  pconnpi1  35824  cvmscbv  35845  cvmsss2  35861  cvmliftlem15  35885  cvmlift2  35903  cvmlift3  35915  elmrsubrn  36107  iprodefisum  36328  cbvprodvw2  36875  cbvitgvw2  36876  knoppcnlem7  37204  knoppf  37240  f1omptsn  38099  mptsnun  38101  fin2so  38369  poimirlem27  38404  broucube  38411  ftc1anclem5  38454  ftc1anclem6  38455  sdclem2  38500  prdstotbnd  38552  prdsbnd2  38553  heiborlem10  38578  lshpkrcl  39997  tendoplcbv  41656  tendo0cbv  41667  tendoicbv  41674  lcfl7N  42382  lcf1o  42432  hdmap1cbv  42683  frlmsnic  43430  evlselv  43443  mzpclval  43578  mzpcompact2lem  43604  rmxyval  43764  dnnumch1  43893  aomclem3  43905  aomclem8  43910  dfac21  43915  pwfi2f1o  43945  dftrcl3  44568  dfrtrcl3  44581  rfovcnvf1od  44852  fsovrfovd  44857  fsovcnvlem  44861  dssmapnvod  44868  clsk3nimkb  44888  radcnvrat  45146  expgrowthi  45165  expgrowth  45167  dvradcnv2  45179  binomcxplemradcnv  45184  binomcxplemdvbinom  45185  binomcxplemdvsum  45187  binomcxplemnotnn0  45188  binomcxp  45189  wessf1ornlem  46025  projf1o  46036  fsumsermpt  46417  fmuldfeqlem1  46420  fprodcn  46438  sumnnodd  46468  limsupvaluz  46544  limsupvaluz2  46574  supcnvlimsup  46576  supcnvlimsupmpt  46577  liminfval2  46604  liminflelimsuplem  46611  fprodsubrecnncnv  46744  fprodaddrecnncnv  46746  dvsinax  46749  fperdvper  46755  dvcosax  46762  ioodvbdlimc1lem1  46767  ioodvbdlimc1  46769  ioodvbdlimc2  46771  dvnmul  46779  dvnprodlem1  46782  dvnprodlem2  46783  dvnprodlem3  46784  dvnprod  46785  itgsin0pilem1  46786  itgiccshift  46816  stoweidlem2  46838  stoweidlem17  46853  stoweidlem32  46868  stoweidlem34  46870  stoweidlem43  46879  stirlinglem2  46911  stirlinglem3  46912  stirlinglem8  46917  dirkerval  46927  dirkerval2  46930  dirkeritg  46938  dirkercncflem3  46941  dirkercncf  46943  fourierdlem14  46957  fourierdlem18  46961  fourierdlem53  46995  fourierdlem62  47004  fourierdlem71  47013  fourierdlem74  47016  fourierdlem75  47017  fourierdlem76  47018  fourierdlem80  47022  fourierdlem81  47023  fourierdlem84  47026  fourierdlem88  47030  fourierdlem92  47034  fourierdlem93  47035  fourierdlem94  47036  fourierdlem95  47037  fourierdlem96  47038  fourierdlem97  47039  fourierdlem98  47040  fourierdlem99  47041  fourierdlem101  47043  fourierdlem103  47045  fourierdlem104  47046  fourierdlem105  47047  fourierdlem106  47048  fourierdlem107  47049  fourierdlem108  47050  fourierdlem110  47052  fourierdlem111  47053  fourierdlem112  47054  fourierdlem113  47055  fourierdlem115  47057  fouriersw  47067  elaa2  47070  etransclem1  47071  etransclem5  47075  etransclem6  47076  etransclem11  47081  etransclem13  47083  etransclem41  47111  etransclem47  47117  etransc  47119  ioorrnopn  47141  ioorrnopnxr  47143  subsaliuncl  47194  sge0resplit  47242  sge0fodjrnlem  47252  nnfoctbdj  47292  iundjiun  47296  voliunsge0lem  47308  meaiuninclem  47316  meaiuninc  47317  meaiininclem  47322  meaiininc  47323  omeiunltfirp  47355  carageniuncllem2  47358  carageniuncl  47359  0ome  47365  isomennd  47367  hoicvrrex  47392  ovn0  47402  ovnsubaddlem2  47407  ovnsubadd  47408  sge0hsphoire  47425  hoidmv1lelem3  47429  hoidmv1le  47430  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  hoidmvlelem5  47435  hoidmvle  47436  ovnhoilem2  47438  ovnhoi  47439  hspmbllem2  47463  hspmbl  47465  hoimbl  47467  opnvonmbllem2  47469  ovnsubadd2  47482  ovolval4  47487  ovolval5lem3  47490  ovnovollem3  47494  iccvonmbl  47515  vonioolem2  47517  vonioo  47518  vonicclem2  47520  vonicc  47521  smflimlem4  47610  smfsuplem2  47648  smflimsuplem1  47656  smflimsuplem8  47663  smflimsup  47664  fundcmpsurbijinjpreimafv  48315  prproropf1o  48415  isuspgrim0  48818  cycldlenngric  48852  isubgr3stgrlem8  48897  rmsupp0  49306  domnmsuppn0  49307  rmsuppss  49308  suppmptcfin  49314  ply1mulgsum  49328  lcoc0  49360  linc1  49363  lcoel0  49366  lcoss  49374  el0ldep  49404  lincresunit3  49419  isldepslvec2  49423  itcovalpclem2  49609  itcovalt2lem2  49614  veronesematrowd  50822  veronesematrowexpd  50823  veroquadgsumlem  50824  veroquadmodzerod  50825  amgmlemALT  50829