Theorem cbvmptv 5208

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 5209 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 2843	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2771	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5182	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5186	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5186	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2793	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  {copab 5166   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-opab 5167  df-mpt 5186

This theorem is used by:  fnmptfvd  7041  mptcnfimad  7999  onnseq  8356  rdgsucmpt2  8442  frsucmpt2  8452  fsetfocdm  8887  fsetprcnex  8888  resixpfo  8968  pw2f1olem  9104  xpmapen  9168  dffi3  9427  ordtypecbv  9515  inf3lema  9629  cantnflem1  9694  cnfcomlem  9704  infxpenc2  10105  fseqenlem1  10107  dfac8a  10113  dfac12r  10229  hfom  10325  fictb  10326  cfsmo  10353  coftr  10355  fin23lem38  10431  compsscnv  10453  isf34lem1  10454  compss  10458  fin1a2lem1  10482  fin1a2lem3  10484  fin1a2lem13  10494  itunisuc  10501  hsmex  10514  domtriom  10525  axdc2  10531  zorn2g  10585  ttukey2g  10598  axdc  10603  konigth  10658  pwcfsdom  10672  canthp1  10743  wunex2  10827  wuncval2  10836  negiso  12301  infrenegsup  12304  rpnnen1  13115  caurcvg2  15851  caucvg  15852  summo  15889  zsum  15890  fsum  15892  ackbijnn  16003  cbvprodv  16089  prodmo  16109  zprod  16110  fprod  16114  iprodmul  16176  bpolyval  16221  phimullem  16962  eulerth  16966  iserodd  17019  prmreclem5  17104  prmrec  17106  vdwlem7  17171  vdwlem9  17173  vdwlem10  17174  ramub1  17212  ramcl  17213  yonedalem4c  18457  yonedalem3b  18459  gsumwspan  19048  smndex1iidm  19103  smndex1gid  19106  smndex1gidOLD  19107  smndex2dlinvh  19122  grplactcnv  19259  gicqusker  19508  galactghm  19624  symgfixfo  19659  pmtrdifwrdel  19705  pmtrdifwrdel2  19706  odf1o2  19793  sylow1lem2  19819  sylow1  19823  sylow2b  19843  sylow3lem1  19847  sylow3lem5  19851  sylow3  19853  efgtf  19942  efgsval  19951  ghmcyg  20116  cycsubgcyg  20121  ablfaclem3  20309  ablfac2  20311  srgbinomlem4  20461  funcrngcsetcALT  20899  fidomndrnglem  21036  isphld  21966  frlmphl  22093  mplmonmul  22351  evlslem2  22394  mat1ric  22808  mdetralt  22929  smadiadetlem3  22989  pmatcollpw3lem  23107  mp2pm2mplem5  23134  mp2pm2mp  23135  pm2mpmhmlem2  23143  cpmidpmat  23197  cpmadugsumlemF  23200  cpmadugsumfi  23201  cpmadumatpoly  23207  chcoeffeqlem  23209  cayleyhamilton0  23213  cayleyhamilton  23214  cayleyhamiltonALT  23215  cayleyhamilton1  23216  ordtbaslem  23512  ordtbas2  23515  lly1stc  23821  ptpjopn  23937  xkohmeo  24140  fbasrn  24209  elfm  24272  tmdmulg  24417  tmdgsum  24420  qustgpopn  24445  tsmsfbas  24453  tsmsf1o  24470  ustuqtoplem  24564  utopsnneip  24573  fmucnd  24616  ucnextcn  24628  met1stc  24846  prdsxmslem2  24854  metustto  24878  metustexhalf  24881  metuust  24885  cfilucfil2  24886  metuel  24889  metuel2  24890  psmetutop  24892  restmetu  24895  metucn  24896  xrge0tsms  25160  metdsge  25175  expcn  25199  pi1xfrcnv  25384  minveclem3b  25755  minveclem5  25760  minvec  25763  ovollb2  25816  ovolshftlem2  25837  ovolscalem2  25841  ovolicc  25850  ioombl1  25889  uniioombllem6  25915  volsup2  25932  vitali  25940  mbfi1fseq  26048  mbfmullem  26052  itg2seq  26069  itg2i1fseq  26082  itg2addlem  26085  itg2cnlem1  26088  itg2cn  26090  cbvitgv  26103  dvfsumrlimge0  26356  plyadd  26542  plymul  26543  coeeu  26550  coeid  26563  dvply2g  26612  plydivex  26624  elqaalem2  26649  elqaa  26651  taylthlem1  26706  taylth  26708  pserval  26743  radcnvlem2  26747  radcnvlt2  26752  dvradcnv  26754  pserulm  26755  psercn  26759  pserdvlem2  26761  pserdv  26762  efgh  26875  eff1olem  26882  circgrp  26886  circsubm  26887  logno1  26970  emcl  27336  harmonicbnd  27337  harmonicbnd2  27338  basel  27423  musum  27524  dchr1  27590  dchrptlem2  27598  dchrpt  27600  lgsqrlem4  27682  lgseisenlem3  27710  2sqlem1  27750  dchrmusumlema  27826  dchrmusum2  27827  dchrvmasumlema  27833  dchrvmasumiflem1  27834  dchrisum0ff  27840  dchrisum0lema  27847  dchrisum0lem1b  27848  dchrisum0lem2a  27850  nosupcbv  28065  noinfcbv  28080  precsexlemcbv  28598  seqsfn  28701  seqsp1  28703  wlknwwlksnbij  30483  clwlkclwwlken  30609  clwlknf1oclwwlkn  30681  frgrncvvdeqlem8  30913  frgrncvvdeqlem9  30914  numclwwlk1lem2  30967  ubthlem3  31480  minveco  31492  htth  31526  fsuppcurry1  33363  fsuppcurry2  33364  gsumhashmul  33675  gsummulsubdishift1  33676  gsummulsubdishift1s  33678  gsummulsubdishift2s  33679  xrge0tsmsd  33681  elrgspnlem1  33850  elrgspnlem2  33851  elrgspn  33854  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  elrgspnsubrun  33857  idomsubr  33918  nsgmgc  34010  nsgqusf1olem1  34011  lmicqusker  34016  ricqusker  34024  elrspunidl  34025  elrspunsn  34026  zringfrac  34133  0mplric  34194  selvply1rhmlemb  34198  selvply1rhmlem3  34201  selvply1rhmlem5  34203  selvply1rhm  34204  mplidom  34207  mplvrpmga  34224  mplvrpmrhm  34226  psrgsum  34227  psrmonmul  34229  psrmonprod  34231  splysubrg  34239  issply  34240  esplyfvaln  34253  vietalem  34258  vieta  34259  ply1degltdim  34302  lbsdiflsp0  34305  fedgmullem1  34308  fedgmul  34310  assarrginv  34315  evls1fldgencl  34349  fldextrspunlsplem  34352  fldextrspunlsp  34353  extdgfialglem2  34372  extdgfialg  34373  algextdeglem4  34399  algextdeg  34404  constrcbvlem  34434  madjusmdetlem2  34507  madjusmdet  34510  zartop  34555  zartopon  34556  zart0  34558  zarmxt1  34559  zarcmp  34561  rhmpreimacn  34564  xrge0mulc1cn  34620  xrge0tmd  34624  xrge0tmdALT  34625  cbvesumv  34722  gsumesum  34738  esumlub  34739  esumpcvgval  34757  esumcvg  34765  esumcvg2  34766  eulerpartlems  35039  eulerpart  35061  fibp1  35080  rrvadd  35131  ballotlemfval  35169  ballotlemi  35180  ballotlemsval  35188  ballotlemsv  35189  ballotlemsf1o  35193  ballotlemrval  35197  ballotlemrinv  35213  signsply0  35227  actfunsnf1o  35280  actfunsnrndisj  35281  itgexpif  35282  hgt750lemb  35332  onvf1odlem3  35953  derangfmla  36042  erdsze  36054  pconnpi1  36089  cvmscbv  36110  cvmsss2  36126  cvmliftlem15  36150  cvmlift2  36168  cvmlift3  36180  elmrsubrn  36372  iprodefisum  36599  cbvprodvw2  37129  cbvitgvw2  37130  knoppcnlem7  37458  knoppf  37494  f1omptsn  38354  mptsnun  38356  fin2so  38624  poimirlem27  38659  broucube  38666  ftc1anclem5  38709  ftc1anclem6  38710  sdclem2  38770  prdstotbnd  38822  prdsbnd2  38823  heiborlem10  38848  lshpkrcl  40267  tendoplcbv  41926  tendo0cbv  41937  tendoicbv  41944  lcfl7N  42652  lcf1o  42702  hdmap1cbv  42953  frlmsnic  43698  evlselv  43711  mzpclval  43830  mzpcompact2lem  43856  rmxyval  44016  dnnumch1  44145  aomclem3  44152  aomclem8  44157  dfac21  44162  pwfi2f1o  44192  dftrcl3  44814  dfrtrcl3  44827  rfovcnvf1od  45098  fsovrfovd  45103  fsovcnvlem  45107  dssmapnvod  45114  clsk3nimkb  45134  radcnvrat  45392  expgrowthi  45411  expgrowth  45413  dvradcnv2  45425  binomcxplemradcnv  45430  binomcxplemdvbinom  45431  binomcxplemdvsum  45433  binomcxplemnotnn0  45434  binomcxp  45435  wessf1ornlem  46294  projf1o  46305  fsumsermpt  46685  fmuldfeqlem1  46688  fprodcn  46706  sumnnodd  46736  limsupvaluz  46812  limsupvaluz2  46842  supcnvlimsup  46844  supcnvlimsupmpt  46845  liminfval2  46872  liminflelimsuplem  46879  fprodsubrecnncnv  47012  fprodaddrecnncnv  47014  dvsinax  47017  fperdvper  47023  dvcosax  47030  ioodvbdlimc1lem1  47035  ioodvbdlimc1  47037  ioodvbdlimc2  47039  dvnmul  47047  dvnprodlem1  47050  dvnprodlem2  47051  dvnprodlem3  47052  dvnprod  47053  itgsin0pilem1  47054  itgiccshift  47084  stoweidlem2  47106  stoweidlem17  47121  stoweidlem32  47136  stoweidlem34  47138  stoweidlem43  47147  stirlinglem2  47179  stirlinglem3  47180  stirlinglem8  47185  dirkerval  47195  dirkerval2  47198  dirkeritg  47206  dirkercncflem3  47209  dirkercncf  47211  fourierdlem14  47225  fourierdlem18  47229  fourierdlem53  47263  fourierdlem62  47272  fourierdlem71  47281  fourierdlem74  47284  fourierdlem75  47285  fourierdlem76  47286  fourierdlem80  47290  fourierdlem81  47291  fourierdlem84  47294  fourierdlem88  47298  fourierdlem92  47302  fourierdlem93  47303  fourierdlem94  47304  fourierdlem95  47305  fourierdlem96  47306  fourierdlem97  47307  fourierdlem98  47308  fourierdlem99  47309  fourierdlem101  47311  fourierdlem103  47313  fourierdlem104  47314  fourierdlem105  47315  fourierdlem106  47316  fourierdlem107  47317  fourierdlem108  47318  fourierdlem110  47320  fourierdlem111  47321  fourierdlem112  47322  fourierdlem113  47323  fourierdlem115  47325  fouriersw  47335  elaa2  47338  etransclem1  47339  etransclem5  47343  etransclem6  47344  etransclem11  47349  etransclem13  47351  etransclem41  47379  etransclem47  47385  etransc  47387  ioorrnopn  47409  ioorrnopnxr  47411  subsaliuncl  47462  sge0resplit  47510  sge0fodjrnlem  47520  nnfoctbdj  47560  iundjiun  47564  voliunsge0lem  47576  meaiuninclem  47584  meaiuninc  47585  meaiininclem  47590  meaiininc  47591  omeiunltfirp  47623  carageniuncllem2  47626  carageniuncl  47627  0ome  47633  isomennd  47635  hoicvrrex  47660  ovn0  47670  ovnsubaddlem2  47675  ovnsubadd  47676  sge0hsphoire  47693  hoidmv1lelem3  47697  hoidmv1le  47698  hoidmvlelem1  47699  hoidmvlelem2  47700  hoidmvlelem3  47701  hoidmvlelem4  47702  hoidmvlelem5  47703  hoidmvle  47704  ovnhoilem2  47706  ovnhoi  47707  hspmbllem2  47731  hspmbl  47733  hoimbl  47735  opnvonmbllem2  47737  ovnsubadd2  47750  ovolval4  47755  ovolval5lem3  47758  ovnovollem3  47762  iccvonmbl  47783  vonioolem2  47785  vonioo  47786  vonicclem2  47788  vonicc  47789  smflimlem4  47878  smfsuplem2  47916  smflimsuplem1  47924  smflimsuplem8  47931  smflimsup  47932  fundcmpsurbijinjpreimafv  48583  prproropf1o  48683  isuspgrim0  49086  cycldlenngric  49120  isubgr3stgrlem8  49165  rmsupp0  49574  domnmsuppn0  49575  rmsuppss  49576  suppmptcfin  49582  ply1mulgsum  49596  lcoc0  49628  linc1  49631  lcoel0  49634  lcoss  49642  el0ldep  49672  lincresunit3  49687  isldepslvec2  49691  itcovalpclem2  49877  itcovalt2lem2  49882  veronesematrowd  51150  veronesematrowexpd  51151  veroquadgsumlem  51152  veroquadmodzerod  51153  amgmlemALT  51157