Theorem cbvmptv 5189

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 5190 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 2819	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2747	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 633	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5163	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5167	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5167	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2769	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  {copab 5147   ↦ cmpt 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-opab 5148  df-mpt 5167

This theorem is referenced by:  fnmptfvd  6993  mptcnfimad  7939  onnseq  8284  rdgsucmpt2  8369  frsucmpt2  8379  fsetfocdm  8808  fsetprcnex  8809  resixpfo  8884  pw2f1olem  9019  xpmapen  9083  dffi3  9344  ordtypecbv  9432  inf3lema  9545  cantnflem1  9610  cnfcomlem  9620  infxpenc2  9944  fseqenlem1  9946  dfac8a  9952  dfac12r  10069  r1om  10165  fictb  10166  cfsmo  10193  coftr  10195  fin23lem38  10271  compsscnv  10293  isf34lem1  10294  compss  10298  fin1a2lem1  10322  fin1a2lem3  10324  fin1a2lem13  10334  itunisuc  10341  hsmex  10354  domtriom  10365  axdc2  10371  zorn2g  10425  ttukey2g  10438  axdc  10443  konigth  10492  pwcfsdom  10506  canthp1  10577  wunex2  10661  wuncval2  10670  negiso  12136  infrenegsup  12139  rpnnen1  12933  caurcvg2  15640  caucvg  15641  summo  15679  zsum  15680  fsum  15682  ackbijnn  15793  cbvprodv  15879  prodmo  15901  zprod  15902  fprod  15906  iprodmul  15968  bpolyval  16014  phimullem  16749  eulerth  16753  iserodd  16806  prmreclem5  16891  prmrec  16893  vdwlem7  16958  vdwlem9  16960  vdwlem10  16961  ramub1  16999  ramcl  17000  yonedalem4c  18243  yonedalem3b  18245  gsumwspan  18814  smndex1iidm  18869  smndex1gid  18872  smndex1gidOLD  18873  smndex2dlinvh  18888  grplactcnv  19019  gicqusker  19263  galactghm  19379  symgfixfo  19414  pmtrdifwrdel  19460  pmtrdifwrdel2  19461  odf1o2  19548  sylow1lem2  19574  sylow1  19578  sylow2b  19598  sylow3lem1  19602  sylow3lem5  19606  sylow3  19608  efgtf  19697  efgsval  19706  ghmcyg  19871  cycsubgcyg  19876  ablfaclem3  20064  ablfac2  20066  srgbinomlem4  20210  funcrngcsetcALT  20618  fidomndrnglem  20749  isphld  21634  frlmphl  21761  mplmonmul  22014  evlslem2  22057  mat1ric  22452  mdetralt  22573  smadiadetlem3  22633  pmatcollpw3lem  22748  mp2pm2mplem5  22775  mp2pm2mp  22776  pm2mpmhmlem2  22784  cpmidpmat  22838  cpmadugsumlemF  22841  cpmadugsumfi  22842  cpmadumatpoly  22848  chcoeffeqlem  22850  cayleyhamilton0  22854  cayleyhamilton  22855  cayleyhamiltonALT  22856  cayleyhamilton1  22857  ordtbaslem  23153  ordtbas2  23156  lly1stc  23461  ptpjopn  23577  xkohmeo  23780  fbasrn  23849  elfm  23912  tmdmulg  24057  tmdgsum  24060  qustgpopn  24085  tsmsfbas  24093  tsmsf1o  24110  ustuqtoplem  24204  utopsnneip  24213  fmucnd  24256  ucnextcn  24268  met1stc  24486  prdsxmslem2  24494  metustto  24518  metustexhalf  24521  metuust  24525  cfilucfil2  24526  metuel  24529  metuel2  24530  psmetutop  24532  restmetu  24535  metucn  24536  xrge0tsms  24800  metdsge  24815  expcn  24839  pi1xfrcnv  25024  minveclem3b  25395  minveclem5  25400  minvec  25403  ovollb2  25456  ovolshftlem2  25477  ovolscalem2  25481  ovolicc  25490  ioombl1  25529  uniioombllem6  25555  volsup2  25572  vitali  25580  mbfi1fseq  25688  mbfmullem  25692  itg2seq  25709  itg2i1fseq  25722  itg2addlem  25725  itg2cnlem1  25728  itg2cn  25730  cbvitgv  25744  dvfsumrlimge0  25997  plyadd  26182  plymul  26183  coeeu  26190  coeid  26203  dvply2g  26251  plydivex  26263  elqaalem2  26286  elqaa  26288  taylthlem1  26338  taylth  26340  pserval  26375  radcnvlem2  26379  radcnvlt2  26384  dvradcnv  26386  pserulm  26387  psercn  26391  pserdvlem2  26393  pserdv  26394  efgh  26505  eff1olem  26512  circgrp  26516  circsubm  26517  logno1  26600  emcl  26966  harmonicbnd  26967  harmonicbnd2  26968  basel  27053  musum  27154  dchr1  27220  dchrptlem2  27228  dchrpt  27230  lgsqrlem4  27312  lgseisenlem3  27340  2sqlem1  27380  dchrmusumlema  27456  dchrmusum2  27457  dchrvmasumlema  27463  dchrvmasumiflem1  27464  dchrisum0ff  27470  dchrisum0lema  27477  dchrisum0lem1b  27478  dchrisum0lem2a  27480  nosupcbv  27666  noinfcbv  27681  precsexlemcbv  28198  seqsfn  28301  seqsp1  28303  wlknwwlksnbij  29956  clwlkclwwlken  30082  clwlknf1oclwwlkn  30154  frgrncvvdeqlem8  30376  frgrncvvdeqlem9  30377  numclwwlk1lem2  30430  ubthlem3  30943  minveco  30955  htth  30989  fsuppcurry1  32797  fsuppcurry2  32798  gsumhashmul  33128  gsummulsubdishift1  33129  gsummulsubdishift1s  33131  gsummulsubdishift2s  33132  xrge0tsmsd  33134  elrgspnlem1  33303  elrgspnlem2  33304  elrgspn  33307  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrgspnsubrun  33310  idomsubr  33370  nsgmgc  33472  nsgqusf1olem1  33473  lmicqusker  33478  ricqusker  33487  elrspunidl  33488  elrspunsn  33489  zringfrac  33614  mplvrpmga  33689  mplvrpmrhm  33691  psrgsum  33692  psrmonmul  33694  psrmonprod  33696  splysubrg  33704  issply  33705  esplyfvaln  33718  vietalem  33723  vieta  33724  ply1degltdim  33767  lbsdiflsp0  33770  fedgmullem1  33773  fedgmul  33775  assarrginv  33780  evls1fldgencl  33814  fldextrspunlsplem  33817  fldextrspunlsp  33818  extdgfialglem2  33837  extdgfialg  33838  algextdeglem4  33864  algextdeg  33869  constrcbvlem  33899  madjusmdetlem2  33972  madjusmdet  33975  zartop  34020  zartopon  34021  zart0  34023  zarmxt1  34024  zarcmp  34026  rhmpreimacn  34029  xrge0mulc1cn  34085  xrge0tmd  34089  xrge0tmdALT  34090  cbvesumv  34187  gsumesum  34203  esumlub  34204  esumpcvgval  34222  esumcvg  34230  esumcvg2  34231  eulerpartlems  34504  eulerpart  34526  fibp1  34545  rrvadd  34596  ballotlemfval  34634  ballotlemi  34645  ballotlemsval  34653  ballotlemsv  34654  ballotlemsf1o  34658  ballotlemrval  34662  ballotlemrinv  34678  signsply0  34695  actfunsnf1o  34748  actfunsnrndisj  34749  itgexpif  34750  hgt750lemb  34800  onvf1odlem3  35287  derangfmla  35372  erdsze  35384  pconnpi1  35419  cvmscbv  35440  cvmsss2  35456  cvmliftlem15  35480  cvmlift2  35498  cvmlift3  35510  elmrsubrn  35702  iprodefisum  35923  cbvprodvw2  36429  cbvitgvw2  36430  knoppcnlem7  36759  knoppf  36795  f1omptsn  37653  mptsnun  37655  fin2so  37928  poimirlem27  37968  broucube  37975  ftc1anclem5  38018  ftc1anclem6  38019  sdclem2  38063  prdstotbnd  38115  prdsbnd2  38116  heiborlem10  38141  lshpkrcl  39562  tendoplcbv  41221  tendo0cbv  41232  tendoicbv  41239  lcfl7N  41947  lcf1o  41997  hdmap1cbv  42248  frlmsnic  42985  evlselv  43020  mzpclval  43157  mzpcompact2lem  43183  rmxyval  43343  dnnumch1  43472  aomclem3  43484  aomclem8  43489  dfac21  43494  pwfi2f1o  43524  dftrcl3  44147  dfrtrcl3  44160  rfovcnvf1od  44431  fsovrfovd  44436  fsovcnvlem  44440  dssmapnvod  44447  clsk3nimkb  44467  radcnvrat  44741  expgrowthi  44760  expgrowth  44762  dvradcnv2  44774  binomcxplemradcnv  44779  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  binomcxp  44784  wessf1ornlem  45615  projf1o  45626  fsumsermpt  46009  fmuldfeqlem1  46012  fprodcn  46030  sumnnodd  46060  limsupvaluz  46136  limsupvaluz2  46166  supcnvlimsup  46168  supcnvlimsupmpt  46169  liminfval2  46196  liminflelimsuplem  46203  fprodsubrecnncnv  46336  fprodaddrecnncnv  46338  dvsinax  46341  fperdvper  46347  dvcosax  46354  ioodvbdlimc1lem1  46359  ioodvbdlimc1  46361  ioodvbdlimc2  46363  dvnmul  46371  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  dvnprod  46377  itgsin0pilem1  46378  itgiccshift  46408  stoweidlem2  46430  stoweidlem17  46445  stoweidlem32  46460  stoweidlem34  46462  stoweidlem43  46471  stirlinglem2  46503  stirlinglem3  46504  stirlinglem8  46509  dirkerval  46519  dirkerval2  46522  dirkeritg  46530  dirkercncflem3  46533  dirkercncf  46535  fourierdlem14  46549  fourierdlem18  46553  fourierdlem53  46587  fourierdlem62  46596  fourierdlem71  46605  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem80  46614  fourierdlem81  46615  fourierdlem84  46618  fourierdlem88  46622  fourierdlem92  46626  fourierdlem93  46627  fourierdlem94  46628  fourierdlem95  46629  fourierdlem96  46630  fourierdlem97  46631  fourierdlem98  46632  fourierdlem99  46633  fourierdlem101  46635  fourierdlem103  46637  fourierdlem104  46638  fourierdlem105  46639  fourierdlem106  46640  fourierdlem107  46641  fourierdlem108  46642  fourierdlem110  46644  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fourierdlem115  46649  fouriersw  46659  elaa2  46662  etransclem1  46663  etransclem5  46667  etransclem6  46668  etransclem11  46673  etransclem13  46675  etransclem41  46703  etransclem47  46709  etransc  46711  ioorrnopn  46733  ioorrnopnxr  46735  subsaliuncl  46786  sge0resplit  46834  sge0fodjrnlem  46844  nnfoctbdj  46884  iundjiun  46888  voliunsge0lem  46900  meaiuninclem  46908  meaiuninc  46909  meaiininclem  46914  meaiininc  46915  omeiunltfirp  46947  carageniuncllem2  46950  carageniuncl  46951  0ome  46957  isomennd  46959  hoicvrrex  46984  ovn0  46994  ovnsubaddlem2  46999  ovnsubadd  47000  sge0hsphoire  47017  hoidmv1lelem3  47021  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hoidmvlelem5  47027  hoidmvle  47028  ovnhoilem2  47030  ovnhoi  47031  hspmbllem2  47055  hspmbl  47057  hoimbl  47059  opnvonmbllem2  47061  ovnsubadd2  47074  ovolval4  47079  ovolval5lem3  47082  ovnovollem3  47086  iccvonmbl  47107  vonioolem2  47109  vonioo  47110  vonicclem2  47112  vonicc  47113  smflimlem4  47202  smfsuplem2  47240  smflimsuplem1  47248  smflimsuplem8  47255  smflimsup  47256  fundcmpsurbijinjpreimafv  47867  prproropf1o  47967  isuspgrim0  48370  cycldlenngric  48404  isubgr3stgrlem8  48449  rmsupp0  48844  domnmsuppn0  48845  rmsuppss  48846  suppmptcfin  48852  ply1mulgsum  48866  lcoc0  48898  linc1  48901  lcoel0  48904  lcoss  48912  el0ldep  48942  lincresunit3  48957  isldepslvec2  48961  itcovalpclem2  49147  itcovalt2lem2  49152  amgmlemALT  50278