Theorem cbvmptv 5260

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 5262 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 2821	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2745	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5226	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5231	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5231	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2772	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536   ∈ wcel 2105  {copab 5209   ↦ cmpt 5230

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5210  df-mpt 5231

This theorem is referenced by:  fnmptfvd  7060  mptcnfimad  8009  onnseq  8382  rdgsucmpt2  8468  frsucmpt2  8478  fsetfocdm  8899  fsetprcnex  8900  resixpfo  8974  pw2f1olem  9114  xpmapen  9183  dffi3  9468  ordtypecbv  9554  inf3lema  9661  cantnflem1  9726  cnfcomlem  9736  infxpenc2  10059  fseqenlem1  10061  dfac8a  10067  dfac12r  10184  r1om  10280  fictb  10281  cfsmo  10308  coftr  10310  fin23lem38  10386  compsscnv  10408  isf34lem1  10409  compss  10413  fin1a2lem1  10437  fin1a2lem3  10439  fin1a2lem13  10449  itunisuc  10456  hsmex  10469  domtriom  10480  axdc2  10486  zorn2g  10540  ttukey2g  10553  axdc  10558  konigth  10606  pwcfsdom  10620  canthp1  10691  wunex2  10775  wuncval2  10784  negiso  12245  infrenegsup  12248  rpnnen1  13022  caurcvg2  15710  caucvg  15711  summo  15749  zsum  15750  fsum  15752  ackbijnn  15860  cbvprodv  15946  prodmo  15968  zprod  15969  fprod  15973  iprodmul  16035  bpolyval  16081  phimullem  16812  eulerth  16816  iserodd  16868  prmreclem5  16953  prmrec  16955  vdwlem7  17020  vdwlem9  17022  vdwlem10  17023  ramub1  17061  ramcl  17062  yonedalem4c  18333  yonedalem3b  18335  gsumwspan  18871  smndex1iidm  18926  smndex1gid  18928  smndex2dlinvh  18942  grplactcnv  19073  gicqusker  19318  galactghm  19436  symgfixfo  19471  pmtrdifwrdel  19517  pmtrdifwrdel2  19518  odf1o2  19605  sylow1lem2  19631  sylow1  19635  sylow2b  19655  sylow3lem1  19659  sylow3lem5  19663  sylow3  19665  efgtf  19754  efgsval  19763  ghmcyg  19928  cycsubgcyg  19933  ablfaclem3  20121  ablfac2  20123  srgbinomlem4  20246  funcrngcsetcALT  20657  fidomndrnglem  20789  isphld  21689  frlmphl  21818  mplmonmul  22071  evlslem2  22120  mat1ric  22508  mdetralt  22629  smadiadetlem3  22689  pmatcollpw3lem  22804  mp2pm2mplem5  22831  mp2pm2mp  22832  pm2mpmhmlem2  22840  cpmidpmat  22894  cpmadugsumlemF  22897  cpmadugsumfi  22898  cpmadumatpoly  22904  chcoeffeqlem  22906  cayleyhamilton0  22910  cayleyhamilton  22911  cayleyhamiltonALT  22912  cayleyhamilton1  22913  ordtbaslem  23211  ordtbas2  23214  lly1stc  23519  ptpjopn  23635  xkohmeo  23838  fbasrn  23907  elfm  23970  tmdmulg  24115  tmdgsum  24118  qustgpopn  24143  tsmsfbas  24151  tsmsf1o  24168  ustuqtoplem  24263  utopsnneip  24272  fmucnd  24316  ucnextcn  24328  met1stc  24549  prdsxmslem2  24557  metustto  24581  metustexhalf  24584  metuust  24588  cfilucfil2  24589  metuel  24592  metuel2  24593  psmetutop  24595  restmetu  24598  metucn  24599  xrge0tsms  24869  metdsge  24884  expcn  24909  expcnOLD  24911  pi1xfrcnv  25103  minveclem3b  25475  minveclem5  25480  minvec  25483  ovollb2  25537  ovolshftlem2  25558  ovolscalem2  25562  ovolicc  25571  ioombl1  25610  uniioombllem6  25636  volsup2  25653  vitali  25661  mbfi1fseq  25770  mbfmullem  25774  itg2seq  25791  itg2i1fseq  25804  itg2addlem  25807  itg2cnlem1  25810  itg2cn  25812  cbvitgv  25826  dvfsumrlimge0  26085  plyadd  26270  plymul  26271  coeeu  26278  coeid  26291  dvply2g  26340  dvply2gOLD  26341  plydivex  26353  elqaalem2  26376  elqaa  26378  taylthlem1  26429  taylth  26432  pserval  26467  radcnvlem2  26471  radcnvlt2  26476  dvradcnv  26478  pserulm  26479  psercn  26484  pserdvlem2  26486  pserdv  26487  efgh  26597  eff1olem  26604  circgrp  26608  circsubm  26609  logno1  26692  emcl  27060  harmonicbnd  27061  harmonicbnd2  27062  basel  27147  musum  27248  dchr1  27315  dchrptlem2  27323  dchrpt  27325  lgsqrlem4  27407  lgseisenlem3  27435  2sqlem1  27475  dchrmusumlema  27551  dchrmusum2  27552  dchrvmasumlema  27558  dchrvmasumiflem1  27559  dchrisum0ff  27565  dchrisum0lema  27572  dchrisum0lem1b  27573  dchrisum0lem2a  27575  nosupcbv  27761  noinfcbv  27776  precsexlemcbv  28244  seqsfn  28329  seqsp1  28331  wlknwwlksnbij  29917  clwlkclwwlken  30040  clwlknf1oclwwlkn  30112  frgrncvvdeqlem8  30334  frgrncvvdeqlem9  30335  numclwwlk1lem2  30388  ubthlem3  30900  minveco  30912  htth  30946  fsuppcurry1  32742  fsuppcurry2  32743  gsumhashmul  33046  xrge0tsmsd  33047  elrgspnlem1  33231  elrgspnlem2  33232  elrgspn  33235  idomsubr  33290  nsgmgc  33419  nsgqusf1olem1  33420  lmicqusker  33425  ricqusker  33434  elrspunidl  33435  elrspunsn  33436  zringfrac  33561  ply1degltdim  33650  lbsdiflsp0  33653  fedgmullem1  33656  fedgmul  33658  assarrginv  33663  evls1fldgencl  33694  algextdeglem4  33725  algextdeg  33730  madjusmdetlem2  33788  madjusmdet  33791  zartop  33836  zartopon  33837  zart0  33839  zarmxt1  33840  zarcmp  33842  rhmpreimacn  33845  xrge0mulc1cn  33901  xrge0tmd  33905  xrge0tmdALT  33906  cbvesumv  34023  gsumesum  34039  esumlub  34040  esumpcvgval  34058  esumcvg  34066  esumcvg2  34067  eulerpartlems  34341  eulerpart  34363  fibp1  34382  rrvadd  34433  ballotlemfval  34470  ballotlemi  34481  ballotlemsval  34489  ballotlemsv  34490  ballotlemsf1o  34494  ballotlemrval  34498  ballotlemrinv  34514  signsply0  34544  actfunsnf1o  34597  actfunsnrndisj  34598  itgexpif  34599  hgt750lemb  34649  derangfmla  35174  erdsze  35186  pconnpi1  35221  cvmscbv  35242  cvmsss2  35258  cvmliftlem15  35282  cvmlift2  35300  cvmlift3  35312  elmrsubrn  35504  iprodefisum  35720  cbvprodvw2  36229  cbvitgvw2  36230  knoppcnlem7  36481  knoppf  36517  f1omptsn  37319  mptsnun  37321  fin2so  37593  poimirlem27  37633  broucube  37640  ftc1anclem5  37683  ftc1anclem6  37684  sdclem2  37728  prdstotbnd  37780  prdsbnd2  37781  heiborlem10  37806  lshpkrcl  39097  tendoplcbv  40757  tendo0cbv  40768  tendoicbv  40775  lcfl7N  41483  lcf1o  41533  hdmap1cbv  41784  frlmsnic  42526  evlselv  42573  mzpclval  42712  mzpcompact2lem  42738  rmxyval  42903  dnnumch1  43032  aomclem3  43044  aomclem8  43049  dfac21  43054  pwfi2f1o  43084  dftrcl3  43709  dfrtrcl3  43722  rfovcnvf1od  43993  fsovrfovd  43998  fsovcnvlem  44002  dssmapnvod  44009  clsk3nimkb  44029  radcnvrat  44309  expgrowthi  44328  expgrowth  44330  dvradcnv2  44342  binomcxplemradcnv  44347  binomcxplemdvbinom  44348  binomcxplemdvsum  44350  binomcxplemnotnn0  44351  binomcxp  44352  wessf1ornlem  45127  projf1o  45139  fsumsermpt  45534  fmuldfeqlem1  45537  fprodcn  45555  sumnnodd  45585  limsupvaluz  45663  limsupvaluz2  45693  supcnvlimsup  45695  supcnvlimsupmpt  45696  liminfval2  45723  liminflelimsuplem  45730  fprodsubrecnncnv  45863  fprodaddrecnncnv  45865  dvsinax  45868  fperdvper  45874  dvcosax  45881  ioodvbdlimc1lem1  45886  ioodvbdlimc1  45888  ioodvbdlimc2  45890  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  dvnprod  45904  itgsin0pilem1  45905  itgiccshift  45935  stoweidlem2  45957  stoweidlem17  45972  stoweidlem32  45987  stoweidlem34  45989  stoweidlem43  45998  stirlinglem2  46030  stirlinglem3  46031  stirlinglem8  46036  dirkerval  46046  dirkerval2  46049  dirkeritg  46057  dirkercncflem3  46060  dirkercncf  46062  fourierdlem14  46076  fourierdlem18  46080  fourierdlem53  46114  fourierdlem62  46123  fourierdlem71  46132  fourierdlem74  46135  fourierdlem75  46136  fourierdlem76  46137  fourierdlem80  46141  fourierdlem81  46142  fourierdlem84  46145  fourierdlem88  46149  fourierdlem92  46153  fourierdlem93  46154  fourierdlem94  46155  fourierdlem95  46156  fourierdlem96  46157  fourierdlem97  46158  fourierdlem98  46159  fourierdlem99  46160  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem105  46166  fourierdlem106  46167  fourierdlem107  46168  fourierdlem108  46169  fourierdlem110  46171  fourierdlem111  46172  fourierdlem112  46173  fourierdlem113  46174  fourierdlem115  46176  fouriersw  46186  elaa2  46189  etransclem1  46190  etransclem5  46194  etransclem6  46195  etransclem11  46200  etransclem13  46202  etransclem41  46230  etransclem47  46236  etransc  46238  ioorrnopn  46260  ioorrnopnxr  46262  subsaliuncl  46313  sge0resplit  46361  sge0fodjrnlem  46371  nnfoctbdj  46411  iundjiun  46415  voliunsge0lem  46427  meaiuninclem  46435  meaiuninc  46436  meaiininclem  46441  meaiininc  46442  omeiunltfirp  46474  carageniuncllem2  46477  carageniuncl  46478  0ome  46484  isomennd  46486  hoicvrrex  46511  ovn0  46521  ovnsubaddlem2  46526  ovnsubadd  46527  sge0hsphoire  46544  hoidmv1lelem3  46548  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hoidmvlelem5  46554  hoidmvle  46555  ovnhoilem2  46557  ovnhoi  46558  hspmbllem2  46582  hspmbl  46584  hoimbl  46586  opnvonmbllem2  46588  ovnsubadd2  46601  ovolval4  46606  ovolval5lem3  46609  ovnovollem3  46613  iccvonmbl  46634  vonioolem2  46636  vonioo  46637  vonicclem2  46639  vonicc  46640  smflimlem4  46729  smfsuplem2  46767  smflimsuplem1  46775  smflimsuplem8  46782  smflimsup  46783  fundcmpsurbijinjpreimafv  47331  prproropf1o  47431  isuspgrim0  47809  uspgrimprop  47810  isubgr3stgrlem8  47875  rmsupp0  48212  domnmsuppn0  48213  rmsuppss  48214  suppmptcfin  48220  ply1mulgsum  48235  lcoc0  48267  linc1  48270  lcoel0  48273  lcoss  48281  el0ldep  48311  lincresunit3  48326  isldepslvec2  48330  itcovalpclem2  48520  itcovalt2lem2  48525  amgmlemALT  49033