Theorem cbvmptv 5203

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 5204 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 2844	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2772	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 641	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5177	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5181	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5181	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2794	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {copab 5161   ↦ cmpt 5180

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-opab 5162  df-mpt 5181

This theorem is referenced by:  fnmptfvd  7018  mptcnfimad  7963  onnseq  8310  rdgsucmpt2  8396  frsucmpt2  8406  fsetfocdm  8838  fsetprcnex  8839  resixpfo  8914  pw2f1olem  9049  xpmapen  9113  dffi3  9374  ordtypecbv  9462  inf3lema  9576  cantnflem1  9641  cnfcomlem  9651  infxpenc2  9975  fseqenlem1  9977  dfac8a  9983  dfac12r  10100  r1om  10196  fictb  10197  cfsmo  10225  coftr  10227  fin23lem38  10303  compsscnv  10325  isf34lem1  10326  compss  10330  fin1a2lem1  10354  fin1a2lem3  10356  fin1a2lem13  10366  itunisuc  10373  hsmex  10386  domtriom  10397  axdc2  10403  zorn2g  10457  ttukey2g  10470  axdc  10475  konigth  10524  pwcfsdom  10538  canthp1  10609  wunex2  10693  wuncval2  10702  negiso  12169  infrenegsup  12172  rpnnen1  12981  caurcvg2  15688  caucvg  15689  summo  15727  zsum  15728  fsum  15730  ackbijnn  15841  cbvprodv  15927  prodmo  15949  zprod  15950  fprod  15954  iprodmul  16016  bpolyval  16062  phimullem  16797  eulerth  16801  iserodd  16854  prmreclem5  16939  prmrec  16941  vdwlem7  17006  vdwlem9  17008  vdwlem10  17009  ramub1  17047  ramcl  17048  yonedalem4c  18292  yonedalem3b  18294  gsumwspan  18863  smndex1iidm  18918  smndex1gid  18921  smndex1gidOLD  18922  smndex2dlinvh  18937  grplactcnv  19068  gicqusker  19311  galactghm  19427  symgfixfo  19462  pmtrdifwrdel  19508  pmtrdifwrdel2  19509  odf1o2  19596  sylow1lem2  19622  sylow1  19626  sylow2b  19646  sylow3lem1  19650  sylow3lem5  19654  sylow3  19656  efgtf  19745  efgsval  19754  ghmcyg  19919  cycsubgcyg  19924  ablfaclem3  20112  ablfac2  20114  srgbinomlem4  20258  funcrngcsetcALT  20670  fidomndrnglem  20801  isphld  21686  frlmphl  21813  mplmonmul  22069  evlslem2  22112  mat1ric  22527  mdetralt  22648  smadiadetlem3  22708  pmatcollpw3lem  22823  mp2pm2mplem5  22850  mp2pm2mp  22851  pm2mpmhmlem2  22859  cpmidpmat  22913  cpmadugsumlemF  22916  cpmadugsumfi  22917  cpmadumatpoly  22923  chcoeffeqlem  22925  cayleyhamilton0  22929  cayleyhamilton  22930  cayleyhamiltonALT  22931  cayleyhamilton1  22932  ordtbaslem  23228  ordtbas2  23231  lly1stc  23536  ptpjopn  23652  xkohmeo  23855  fbasrn  23924  elfm  23987  tmdmulg  24132  tmdgsum  24135  qustgpopn  24160  tsmsfbas  24168  tsmsf1o  24185  ustuqtoplem  24279  utopsnneip  24288  fmucnd  24331  ucnextcn  24343  met1stc  24561  prdsxmslem2  24569  metustto  24593  metustexhalf  24596  metuust  24600  cfilucfil2  24601  metuel  24604  metuel2  24605  psmetutop  24607  restmetu  24610  metucn  24611  xrge0tsms  24875  metdsge  24890  expcn  24914  pi1xfrcnv  25099  minveclem3b  25470  minveclem5  25475  minvec  25478  ovollb2  25531  ovolshftlem2  25552  ovolscalem2  25556  ovolicc  25565  ioombl1  25604  uniioombllem6  25630  volsup2  25647  vitali  25655  mbfi1fseq  25763  mbfmullem  25767  itg2seq  25784  itg2i1fseq  25797  itg2addlem  25800  itg2cnlem1  25803  itg2cn  25805  cbvitgv  25819  dvfsumrlimge0  26072  plyadd  26257  plymul  26258  coeeu  26265  coeid  26278  dvply2g  26326  plydivex  26338  elqaalem2  26361  elqaa  26363  taylthlem1  26413  taylth  26415  pserval  26450  radcnvlem2  26454  radcnvlt2  26459  dvradcnv  26461  pserulm  26462  psercn  26466  pserdvlem2  26468  pserdv  26469  efgh  26583  eff1olem  26590  circgrp  26594  circsubm  26595  logno1  26678  emcl  27044  harmonicbnd  27045  harmonicbnd2  27046  basel  27131  musum  27232  dchr1  27298  dchrptlem2  27306  dchrpt  27308  lgsqrlem4  27390  lgseisenlem3  27418  2sqlem1  27458  dchrmusumlema  27534  dchrmusum2  27535  dchrvmasumlema  27541  dchrvmasumiflem1  27542  dchrisum0ff  27548  dchrisum0lema  27555  dchrisum0lem1b  27556  dchrisum0lem2a  27558  nosupcbv  27743  noinfcbv  27758  precsexlemcbv  28276  seqsfn  28379  seqsp1  28381  wlknwwlksnbij  30034  clwlkclwwlken  30160  clwlknf1oclwwlkn  30232  frgrncvvdeqlem8  30454  frgrncvvdeqlem9  30455  numclwwlk1lem2  30508  ubthlem3  31021  minveco  31033  htth  31067  fsuppcurry1  32876  fsuppcurry2  32877  gsumhashmul  33208  gsummulsubdishift1  33209  gsummulsubdishift1s  33211  gsummulsubdishift2s  33212  xrge0tsmsd  33214  elrgspnlem1  33384  elrgspnlem2  33385  elrgspn  33388  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  elrgspnsubrun  33391  idomsubr  33457  nsgmgc  33559  nsgqusf1olem1  33560  lmicqusker  33565  ricqusker  33574  elrspunidl  33575  elrspunsn  33576  zringfrac  33711  0mplric  33773  selvply1rhmlemb  33777  selvply1rhmlem3  33780  selvply1rhmlem5  33782  selvply1rhm  33783  mplidom  33786  mplvrpmga  33803  mplvrpmrhm  33805  psrgsum  33806  psrmonmul  33808  psrmonprod  33810  splysubrg  33818  issply  33819  esplyfvaln  33832  vietalem  33837  vieta  33838  ply1degltdim  33881  lbsdiflsp0  33884  fedgmullem1  33887  fedgmul  33889  assarrginv  33894  evls1fldgencl  33928  fldextrspunlsplem  33931  fldextrspunlsp  33932  extdgfialglem2  33951  extdgfialg  33952  algextdeglem4  33978  algextdeg  33983  constrcbvlem  34013  madjusmdetlem2  34086  madjusmdet  34089  zartop  34134  zartopon  34135  zart0  34137  zarmxt1  34138  zarcmp  34140  rhmpreimacn  34143  xrge0mulc1cn  34199  xrge0tmd  34203  xrge0tmdALT  34204  cbvesumv  34301  gsumesum  34317  esumlub  34318  esumpcvgval  34336  esumcvg  34344  esumcvg2  34345  eulerpartlems  34618  eulerpart  34640  fibp1  34659  rrvadd  34710  ballotlemfval  34748  ballotlemi  34759  ballotlemsval  34767  ballotlemsv  34768  ballotlemsf1o  34772  ballotlemrval  34776  ballotlemrinv  34792  signsply0  34809  actfunsnf1o  34862  actfunsnrndisj  34863  itgexpif  34864  hgt750lemb  34914  onvf1odlem3  35412  derangfmla  35504  erdsze  35516  pconnpi1  35551  cvmscbv  35572  cvmsss2  35588  cvmliftlem15  35612  cvmlift2  35630  cvmlift3  35642  elmrsubrn  35834  iprodefisum  36055  cbvprodvw2  36571  cbvitgvw2  36572  knoppcnlem7  36901  knoppf  36937  f1omptsn  37795  mptsnun  37797  fin2so  38070  poimirlem27  38110  broucube  38117  ftc1anclem5  38160  ftc1anclem6  38161  sdclem2  38205  prdstotbnd  38257  prdsbnd2  38258  heiborlem10  38283  lshpkrcl  39704  tendoplcbv  41363  tendo0cbv  41374  tendoicbv  41381  lcfl7N  42089  lcf1o  42139  hdmap1cbv  42390  frlmsnic  43122  evlselv  43135  mzpclval  43270  mzpcompact2lem  43296  rmxyval  43456  dnnumch1  43585  aomclem3  43597  aomclem8  43602  dfac21  43607  pwfi2f1o  43637  dftrcl3  44260  dfrtrcl3  44273  rfovcnvf1od  44544  fsovrfovd  44549  fsovcnvlem  44553  dssmapnvod  44560  clsk3nimkb  44580  radcnvrat  44854  expgrowthi  44873  expgrowth  44875  dvradcnv2  44887  binomcxplemradcnv  44892  binomcxplemdvbinom  44893  binomcxplemdvsum  44895  binomcxplemnotnn0  44896  binomcxp  44897  wessf1ornlem  45727  projf1o  45738  fsumsermpt  46119  fmuldfeqlem1  46122  fprodcn  46140  sumnnodd  46170  limsupvaluz  46246  limsupvaluz2  46276  supcnvlimsup  46278  supcnvlimsupmpt  46279  liminfval2  46306  liminflelimsuplem  46313  fprodsubrecnncnv  46446  fprodaddrecnncnv  46448  dvsinax  46451  fperdvper  46457  dvcosax  46464  ioodvbdlimc1lem1  46469  ioodvbdlimc1  46471  ioodvbdlimc2  46473  dvnmul  46481  dvnprodlem1  46484  dvnprodlem2  46485  dvnprodlem3  46486  dvnprod  46487  itgsin0pilem1  46488  itgiccshift  46518  stoweidlem2  46540  stoweidlem17  46555  stoweidlem32  46570  stoweidlem34  46572  stoweidlem43  46581  stirlinglem2  46613  stirlinglem3  46614  stirlinglem8  46619  dirkerval  46629  dirkerval2  46632  dirkeritg  46640  dirkercncflem3  46643  dirkercncf  46645  fourierdlem14  46659  fourierdlem18  46663  fourierdlem53  46697  fourierdlem62  46706  fourierdlem71  46715  fourierdlem74  46718  fourierdlem75  46719  fourierdlem76  46720  fourierdlem80  46724  fourierdlem81  46725  fourierdlem84  46728  fourierdlem88  46732  fourierdlem92  46736  fourierdlem93  46737  fourierdlem94  46738  fourierdlem95  46739  fourierdlem96  46740  fourierdlem97  46741  fourierdlem98  46742  fourierdlem99  46743  fourierdlem101  46745  fourierdlem103  46747  fourierdlem104  46748  fourierdlem105  46749  fourierdlem106  46750  fourierdlem107  46751  fourierdlem108  46752  fourierdlem110  46754  fourierdlem111  46755  fourierdlem112  46756  fourierdlem113  46757  fourierdlem115  46759  fouriersw  46769  elaa2  46772  etransclem1  46773  etransclem5  46777  etransclem6  46778  etransclem11  46783  etransclem13  46785  etransclem41  46813  etransclem47  46819  etransc  46821  ioorrnopn  46843  ioorrnopnxr  46845  subsaliuncl  46896  sge0resplit  46944  sge0fodjrnlem  46954  nnfoctbdj  46994  iundjiun  46998  voliunsge0lem  47010  meaiuninclem  47018  meaiuninc  47019  meaiininclem  47024  meaiininc  47025  omeiunltfirp  47057  carageniuncllem2  47060  carageniuncl  47061  0ome  47067  isomennd  47069  hoicvrrex  47094  ovn0  47104  ovnsubaddlem2  47109  ovnsubadd  47110  sge0hsphoire  47127  hoidmv1lelem3  47131  hoidmv1le  47132  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  hoidmvlelem4  47136  hoidmvlelem5  47137  hoidmvle  47138  ovnhoilem2  47140  ovnhoi  47141  hspmbllem2  47165  hspmbl  47167  hoimbl  47169  opnvonmbllem2  47171  ovnsubadd2  47184  ovolval4  47189  ovolval5lem3  47192  ovnovollem3  47196  iccvonmbl  47217  vonioolem2  47219  vonioo  47220  vonicclem2  47222  vonicc  47223  smflimlem4  47312  smfsuplem2  47350  smflimsuplem1  47358  smflimsuplem8  47365  smflimsup  47366  fundcmpsurbijinjpreimafv  47977  prproropf1o  48077  isuspgrim0  48480  cycldlenngric  48514  isubgr3stgrlem8  48559  rmsupp0  48954  domnmsuppn0  48955  rmsuppss  48956  suppmptcfin  48962  ply1mulgsum  48976  lcoc0  49008  linc1  49011  lcoel0  49014  lcoss  49022  el0ldep  49052  lincresunit3  49067  isldepslvec2  49071  itcovalpclem2  49257  itcovalt2lem2  49262  amgmlemALT  50388