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 2847	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2774	. . . 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 2796	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-opab 5172  df-mpt 5191

This theorem is used by:  fnmptfvd  7066  mptcnfimad  8025  onnseq  8383  rdgsucmpt2  8469  frsucmpt2  8479  fsetfocdm  8914  fsetprcnex  8915  resixpfo  8995  pw2f1olem  9131  xpmapen  9195  dffi3  9453  ordtypecbv  9541  inf3lema  9655  cantnflem1  9720  cnfcomlem  9730  infxpenc2  10131  fseqenlem1  10133  dfac8a  10139  dfac12r  10255  hfom  10351  fictb  10352  cfsmo  10379  coftr  10381  fin23lem38  10457  compsscnv  10479  isf34lem1  10480  compss  10484  fin1a2lem1  10508  fin1a2lem3  10510  fin1a2lem13  10520  itunisuc  10527  hsmex  10540  domtriom  10551  axdc2  10557  zorn2g  10611  ttukey2g  10624  axdc  10629  konigth  10684  pwcfsdom  10698  canthp1  10769  wunex2  10853  wuncval2  10862  negiso  12327  infrenegsup  12330  rpnnen1  13141  caurcvg2  15877  caucvg  15878  summo  15915  zsum  15916  fsum  15918  ackbijnn  16029  cbvprodv  16115  prodmo  16135  zprod  16136  fprod  16140  iprodmul  16202  bpolyval  16247  phimullem  16988  eulerth  16992  iserodd  17045  prmreclem5  17130  prmrec  17132  vdwlem7  17197  vdwlem9  17199  vdwlem10  17200  ramub1  17238  ramcl  17239  yonedalem4c  18483  yonedalem3b  18485  gsumwspan  19074  smndex1iidm  19129  smndex1gid  19132  smndex1gidOLD  19133  smndex2dlinvh  19148  grplactcnv  19285  gicqusker  19535  galactghm  19651  symgfixfo  19686  pmtrdifwrdel  19732  pmtrdifwrdel2  19733  odf1o2  19820  sylow1lem2  19846  sylow1  19850  sylow2b  19870  sylow3lem1  19874  sylow3lem5  19878  sylow3  19880  efgtf  19969  efgsval  19978  ghmcyg  20143  cycsubgcyg  20148  ablfaclem3  20336  ablfac2  20338  srgbinomlem4  20488  funcrngcsetcALT  20926  fidomndrnglem  21063  isphld  21993  frlmphl  22120  mplmonmul  22378  evlslem2  22421  mat1ric  22835  mdetralt  22956  smadiadetlem3  23016  pmatcollpw3lem  23134  mp2pm2mplem5  23161  mp2pm2mp  23162  pm2mpmhmlem2  23170  cpmidpmat  23224  cpmadugsumlemF  23227  cpmadugsumfi  23228  cpmadumatpoly  23234  chcoeffeqlem  23236  cayleyhamilton0  23240  cayleyhamilton  23241  cayleyhamiltonALT  23242  cayleyhamilton1  23243  ordtbaslem  23539  ordtbas2  23542  lly1stc  23848  ptpjopn  23964  xkohmeo  24167  fbasrn  24236  elfm  24299  tmdmulg  24444  tmdgsum  24447  qustgpopn  24472  tsmsfbas  24480  tsmsf1o  24497  ustuqtoplem  24591  utopsnneip  24600  fmucnd  24643  ucnextcn  24655  met1stc  24873  prdsxmslem2  24881  metustto  24905  metustexhalf  24908  metuust  24912  cfilucfil2  24913  metuel  24916  metuel2  24917  psmetutop  24919  restmetu  24922  metucn  24923  xrge0tsms  25187  metdsge  25202  expcn  25226  pi1xfrcnv  25411  minveclem3b  25782  minveclem5  25787  minvec  25790  ovollb2  25843  ovolshftlem2  25864  ovolscalem2  25868  ovolicc  25877  ioombl1  25916  uniioombllem6  25942  volsup2  25959  vitali  25967  mbfi1fseq  26075  mbfmullem  26079  itg2seq  26096  itg2i1fseq  26109  itg2addlem  26112  itg2cnlem1  26115  itg2cn  26117  cbvitgv  26130  dvfsumrlimge0  26383  plyadd  26569  plymul  26570  coeeu  26577  coeid  26590  dvply2g  26639  plydivex  26651  elqaalem2  26676  elqaa  26678  taylthlem1  26733  taylth  26735  pserval  26770  radcnvlem2  26774  radcnvlt2  26779  dvradcnv  26781  pserulm  26782  psercn  26786  pserdvlem2  26788  pserdv  26789  efgh  26902  eff1olem  26909  circgrp  26913  circsubm  26914  logno1  26997  emcl  27363  harmonicbnd  27364  harmonicbnd2  27365  basel  27450  musum  27551  dchr1  27617  dchrptlem2  27625  dchrpt  27627  lgsqrlem4  27709  lgseisenlem3  27737  2sqlem1  27777  dchrmusumlema  27853  dchrmusum2  27854  dchrvmasumlema  27860  dchrvmasumiflem1  27861  dchrisum0ff  27867  dchrisum0lema  27874  dchrisum0lem1b  27875  dchrisum0lem2a  27877  nosupcbv  28092  noinfcbv  28107  precsexlemcbv  28625  seqsfn  28728  seqsp1  28730  wlknwwlksnbij  30510  clwlkclwwlken  30636  clwlknf1oclwwlkn  30708  frgrncvvdeqlem8  30940  frgrncvvdeqlem9  30941  numclwwlk1lem2  30994  ubthlem3  31507  minveco  31519  htth  31553  fsuppcurry1  33389  fsuppcurry2  33390  gsumhashmul  33704  gsummulsubdishift1  33705  gsummulsubdishift1s  33707  gsummulsubdishift2s  33708  xrge0tsmsd  33710  elrgspnlem1  33879  elrgspnlem2  33880  elrgspn  33883  elrgspnsubrunlem1  33884  elrgspnsubrunlem2  33885  elrgspnsubrun  33886  idomsubr  33955  nsgmgc  34047  nsgqusf1olem1  34048  lmicqusker  34053  ricqusker  34061  elrspunidl  34062  elrspunsn  34063  zringfrac  34169  0mplric  34230  selvply1rhmlemb  34234  selvply1rhmlem3  34237  selvply1rhmlem5  34239  selvply1rhm  34240  mplidom  34243  mplvrpmga  34260  mplvrpmrhm  34262  psrgsum  34263  psrmonmul  34265  psrmonprod  34267  splysubrg  34275  issply  34276  esplyfvaln  34289  vietalem  34294  vieta  34295  ply1degltdim  34338  lbsdiflsp0  34341  fedgmullem1  34344  fedgmul  34346  assarrginv  34351  evls1fldgencl  34385  fldextrspunlsplem  34388  fldextrspunlsp  34389  extdgfialglem2  34408  extdgfialg  34409  algextdeglem4  34435  algextdeg  34440  constrcbvlem  34470  madjusmdetlem2  34543  madjusmdet  34546  zartop  34591  zartopon  34592  zart0  34594  zarmxt1  34595  zarcmp  34597  rhmpreimacn  34600  xrge0mulc1cn  34656  xrge0tmd  34660  xrge0tmdALT  34661  cbvesumv  34758  gsumesum  34774  esumlub  34775  esumpcvgval  34793  esumcvg  34801  esumcvg2  34802  eulerpartlems  35075  eulerpart  35097  fibp1  35116  rrvadd  35167  ballotlemfval  35205  ballotlemi  35216  ballotlemsval  35224  ballotlemsv  35225  ballotlemsf1o  35229  ballotlemrval  35233  ballotlemrinv  35249  signsply0  35263  actfunsnf1o  35316  actfunsnrndisj  35317  itgexpif  35318  hgt750lemb  35368  onvf1odlem3  36046  derangfmla  36135  erdsze  36147  pconnpi1  36182  cvmscbv  36203  cvmsss2  36219  cvmliftlem15  36243  cvmlift2  36261  cvmlift3  36273  elmrsubrn  36465  iprodefisum  36697  cbvprodvw2  37227  cbvitgvw2  37228  knoppcnlem7  37556  knoppf  37592  f1omptsn  38465  mptsnun  38467  fin2so  38735  poimirlem27  38770  broucube  38777  ftc1anclem5  38820  ftc1anclem6  38821  sdclem2  38879  prdstotbnd  38931  prdsbnd2  38932  heiborlem10  38957  lshpkrcl  40376  tendoplcbv  42035  tendo0cbv  42046  tendoicbv  42053  lcfl7N  42761  lcf1o  42811  hdmap1cbv  43062  frlmsnic  43808  evlselv  43821  mzpclval  43940  mzpcompact2lem  43966  rmxyval  44126  dnnumch1  44255  aomclem3  44262  aomclem8  44267  dfac21  44272  pwfi2f1o  44302  dftrcl3  44923  dfrtrcl3  44936  rfovcnvf1od  45207  fsovrfovd  45212  fsovcnvlem  45216  dssmapnvod  45223  clsk3nimkb  45243  radcnvrat  45501  expgrowthi  45520  expgrowth  45522  dvradcnv2  45534  binomcxplemradcnv  45539  binomcxplemdvbinom  45540  binomcxplemdvsum  45542  binomcxplemnotnn0  45543  binomcxp  45544  ackbij3  46231  wessf1ornlem  46415  projf1o  46426  fsumsermpt  46806  fmuldfeqlem1  46809  fprodcn  46827  sumnnodd  46857  limsupvaluz  46933  limsupvaluz2  46963  supcnvlimsup  46965  supcnvlimsupmpt  46966  liminfval2  46993  liminflelimsuplem  47000  fprodsubrecnncnv  47133  fprodaddrecnncnv  47135  dvsinax  47138  fperdvper  47144  dvcosax  47151  ioodvbdlimc1lem1  47156  ioodvbdlimc1  47158  ioodvbdlimc2  47160  dvnmul  47168  dvnprodlem1  47171  dvnprodlem2  47172  dvnprodlem3  47173  dvnprod  47174  itgsin0pilem1  47175  itgiccshift  47205  stoweidlem2  47227  stoweidlem17  47242  stoweidlem32  47257  stoweidlem34  47259  stoweidlem43  47268  stirlinglem2  47300  stirlinglem3  47301  stirlinglem8  47306  dirkerval  47316  dirkerval2  47319  dirkeritg  47327  dirkercncflem3  47330  dirkercncf  47332  fourierdlem14  47346  fourierdlem18  47350  fourierdlem53  47384  fourierdlem62  47393  fourierdlem71  47402  fourierdlem74  47405  fourierdlem75  47406  fourierdlem76  47407  fourierdlem80  47411  fourierdlem81  47412  fourierdlem84  47415  fourierdlem88  47419  fourierdlem92  47423  fourierdlem93  47424  fourierdlem94  47425  fourierdlem95  47426  fourierdlem96  47427  fourierdlem97  47428  fourierdlem98  47429  fourierdlem99  47430  fourierdlem101  47432  fourierdlem103  47434  fourierdlem104  47435  fourierdlem105  47436  fourierdlem106  47437  fourierdlem107  47438  fourierdlem108  47439  fourierdlem110  47441  fourierdlem111  47442  fourierdlem112  47443  fourierdlem113  47444  fourierdlem115  47446  fouriersw  47456  elaa2  47459  etransclem1  47460  etransclem5  47464  etransclem6  47465  etransclem11  47470  etransclem13  47472  etransclem41  47500  etransclem47  47506  etransc  47508  ioorrnopn  47530  ioorrnopnxr  47532  subsaliuncl  47583  sge0resplit  47631  sge0fodjrnlem  47641  nnfoctbdj  47681  iundjiun  47685  voliunsge0lem  47697  meaiuninclem  47705  meaiuninc  47706  meaiininclem  47711  meaiininc  47712  omeiunltfirp  47744  carageniuncllem2  47747  carageniuncl  47748  0ome  47754  isomennd  47756  hoicvrrex  47781  ovn0  47791  ovnsubaddlem2  47796  ovnsubadd  47797  sge0hsphoire  47814  hoidmv1lelem3  47818  hoidmv1le  47819  hoidmvlelem1  47820  hoidmvlelem2  47821  hoidmvlelem3  47822  hoidmvlelem4  47823  hoidmvlelem5  47824  hoidmvle  47825  ovnhoilem2  47827  ovnhoi  47828  hspmbllem2  47852  hspmbl  47854  hoimbl  47856  opnvonmbllem2  47858  ovnsubadd2  47871  ovolval4  47876  ovolval5lem3  47879  ovnovollem3  47883  iccvonmbl  47904  vonioolem2  47906  vonioo  47907  vonicclem2  47909  vonicc  47910  smflimlem4  47999  smfsuplem2  48037  smflimsuplem1  48045  smflimsuplem8  48052  smflimsup  48053  fundcmpsurbijinjpreimafv  48704  prproropf1o  48804  isuspgrim0  49207  cycldlenngric  49241  isubgr3stgrlem8  49286  rmsupp0  49695  domnmsuppn0  49696  rmsuppss  49697  suppmptcfin  49703  ply1mulgsum  49717  lcoc0  49749  linc1  49752  lcoel0  49755  lcoss  49763  el0ldep  49793  lincresunit3  49808  isldepslvec2  49812  itcovalpclem2  49998  itcovalt2lem2  50003  veronesematrowd  51293  veronesematrowexpd  51294  veroquadgsumlem  51295  veroquadmodzerod  51296  amgmlemALT  51300