Theorem cbvmptv 5211

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 5212 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 2811	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2740	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5185	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5189	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5189	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2762	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {copab 5169   ↦ cmpt 5188

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-mpt 5189

This theorem is referenced by:  fnmptfvd  7013  mptcnfimad  7965  onnseq  8313  rdgsucmpt2  8398  frsucmpt2  8408  fsetfocdm  8834  fsetprcnex  8835  resixpfo  8909  pw2f1olem  9045  xpmapen  9109  dffi3  9382  ordtypecbv  9470  inf3lema  9577  cantnflem1  9642  cnfcomlem  9652  infxpenc2  9975  fseqenlem1  9977  dfac8a  9983  dfac12r  10100  r1om  10196  fictb  10197  cfsmo  10224  coftr  10226  fin23lem38  10302  compsscnv  10324  isf34lem1  10325  compss  10329  fin1a2lem1  10353  fin1a2lem3  10355  fin1a2lem13  10365  itunisuc  10372  hsmex  10385  domtriom  10396  axdc2  10402  zorn2g  10456  ttukey2g  10469  axdc  10474  konigth  10522  pwcfsdom  10536  canthp1  10607  wunex2  10691  wuncval2  10700  negiso  12163  infrenegsup  12166  rpnnen1  12942  caurcvg2  15644  caucvg  15645  summo  15683  zsum  15684  fsum  15686  ackbijnn  15794  cbvprodv  15880  prodmo  15902  zprod  15903  fprod  15907  iprodmul  15969  bpolyval  16015  phimullem  16749  eulerth  16753  iserodd  16806  prmreclem5  16891  prmrec  16893  vdwlem7  16958  vdwlem9  16960  vdwlem10  16961  ramub1  16999  ramcl  17000  yonedalem4c  18238  yonedalem3b  18240  gsumwspan  18773  smndex1iidm  18828  smndex1gid  18830  smndex2dlinvh  18844  grplactcnv  18975  gicqusker  19220  galactghm  19334  symgfixfo  19369  pmtrdifwrdel  19415  pmtrdifwrdel2  19416  odf1o2  19503  sylow1lem2  19529  sylow1  19533  sylow2b  19553  sylow3lem1  19557  sylow3lem5  19561  sylow3  19563  efgtf  19652  efgsval  19661  ghmcyg  19826  cycsubgcyg  19831  ablfaclem3  20019  ablfac2  20021  srgbinomlem4  20138  funcrngcsetcALT  20550  fidomndrnglem  20681  isphld  21563  frlmphl  21690  mplmonmul  21943  evlslem2  21986  mat1ric  22374  mdetralt  22495  smadiadetlem3  22555  pmatcollpw3lem  22670  mp2pm2mplem5  22697  mp2pm2mp  22698  pm2mpmhmlem2  22706  cpmidpmat  22760  cpmadugsumlemF  22763  cpmadugsumfi  22764  cpmadumatpoly  22770  chcoeffeqlem  22772  cayleyhamilton0  22776  cayleyhamilton  22777  cayleyhamiltonALT  22778  cayleyhamilton1  22779  ordtbaslem  23075  ordtbas2  23078  lly1stc  23383  ptpjopn  23499  xkohmeo  23702  fbasrn  23771  elfm  23834  tmdmulg  23979  tmdgsum  23982  qustgpopn  24007  tsmsfbas  24015  tsmsf1o  24032  ustuqtoplem  24127  utopsnneip  24136  fmucnd  24179  ucnextcn  24191  met1stc  24409  prdsxmslem2  24417  metustto  24441  metustexhalf  24444  metuust  24448  cfilucfil2  24449  metuel  24452  metuel2  24453  psmetutop  24455  restmetu  24458  metucn  24459  xrge0tsms  24723  metdsge  24738  expcn  24763  expcnOLD  24765  pi1xfrcnv  24957  minveclem3b  25328  minveclem5  25333  minvec  25336  ovollb2  25390  ovolshftlem2  25411  ovolscalem2  25415  ovolicc  25424  ioombl1  25463  uniioombllem6  25489  volsup2  25506  vitali  25514  mbfi1fseq  25622  mbfmullem  25626  itg2seq  25643  itg2i1fseq  25656  itg2addlem  25659  itg2cnlem1  25662  itg2cn  25664  cbvitgv  25678  dvfsumrlimge0  25937  plyadd  26122  plymul  26123  coeeu  26130  coeid  26143  dvply2g  26192  dvply2gOLD  26193  plydivex  26205  elqaalem2  26228  elqaa  26230  taylthlem1  26281  taylth  26284  pserval  26319  radcnvlem2  26323  radcnvlt2  26328  dvradcnv  26330  pserulm  26331  psercn  26336  pserdvlem2  26338  pserdv  26339  efgh  26450  eff1olem  26457  circgrp  26461  circsubm  26462  logno1  26545  emcl  26913  harmonicbnd  26914  harmonicbnd2  26915  basel  27000  musum  27101  dchr1  27168  dchrptlem2  27176  dchrpt  27178  lgsqrlem4  27260  lgseisenlem3  27288  2sqlem1  27328  dchrmusumlema  27404  dchrmusum2  27405  dchrvmasumlema  27411  dchrvmasumiflem1  27412  dchrisum0ff  27418  dchrisum0lema  27425  dchrisum0lem1b  27426  dchrisum0lem2a  27428  nosupcbv  27614  noinfcbv  27629  precsexlemcbv  28108  seqsfn  28203  seqsp1  28205  wlknwwlksnbij  29818  clwlkclwwlken  29941  clwlknf1oclwwlkn  30013  frgrncvvdeqlem8  30235  frgrncvvdeqlem9  30236  numclwwlk1lem2  30289  ubthlem3  30801  minveco  30813  htth  30847  fsuppcurry1  32648  fsuppcurry2  32649  gsumhashmul  33001  xrge0tsmsd  33002  elrgspnlem1  33193  elrgspnlem2  33194  elrgspn  33197  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrgspnsubrun  33200  idomsubr  33259  nsgmgc  33383  nsgqusf1olem1  33384  lmicqusker  33389  ricqusker  33398  elrspunidl  33399  elrspunsn  33400  zringfrac  33525  ply1degltdim  33619  lbsdiflsp0  33622  fedgmullem1  33625  fedgmul  33627  assarrginv  33632  evls1fldgencl  33665  fldextrspunlsplem  33668  fldextrspunlsp  33669  algextdeglem4  33710  algextdeg  33715  constrcbvlem  33745  madjusmdetlem2  33818  madjusmdet  33821  zartop  33866  zartopon  33867  zart0  33869  zarmxt1  33870  zarcmp  33872  rhmpreimacn  33875  xrge0mulc1cn  33931  xrge0tmd  33935  xrge0tmdALT  33936  cbvesumv  34033  gsumesum  34049  esumlub  34050  esumpcvgval  34068  esumcvg  34076  esumcvg2  34077  eulerpartlems  34351  eulerpart  34373  fibp1  34392  rrvadd  34443  ballotlemfval  34481  ballotlemi  34492  ballotlemsval  34500  ballotlemsv  34501  ballotlemsf1o  34505  ballotlemrval  34509  ballotlemrinv  34525  signsply0  34542  actfunsnf1o  34595  actfunsnrndisj  34596  itgexpif  34597  hgt750lemb  34647  onvf1odlem3  35092  derangfmla  35177  erdsze  35189  pconnpi1  35224  cvmscbv  35245  cvmsss2  35261  cvmliftlem15  35285  cvmlift2  35303  cvmlift3  35315  elmrsubrn  35507  iprodefisum  35728  cbvprodvw2  36235  cbvitgvw2  36236  knoppcnlem7  36487  knoppf  36523  f1omptsn  37325  mptsnun  37327  fin2so  37601  poimirlem27  37641  broucube  37648  ftc1anclem5  37691  ftc1anclem6  37692  sdclem2  37736  prdstotbnd  37788  prdsbnd2  37789  heiborlem10  37814  lshpkrcl  39109  tendoplcbv  40769  tendo0cbv  40780  tendoicbv  40787  lcfl7N  41495  lcf1o  41545  hdmap1cbv  41796  frlmsnic  42528  evlselv  42575  mzpclval  42713  mzpcompact2lem  42739  rmxyval  42904  dnnumch1  43033  aomclem3  43045  aomclem8  43050  dfac21  43055  pwfi2f1o  43085  dftrcl3  43709  dfrtrcl3  43722  rfovcnvf1od  43993  fsovrfovd  43998  fsovcnvlem  44002  dssmapnvod  44009  clsk3nimkb  44029  radcnvrat  44303  expgrowthi  44322  expgrowth  44324  dvradcnv2  44336  binomcxplemradcnv  44341  binomcxplemdvbinom  44342  binomcxplemdvsum  44344  binomcxplemnotnn0  44345  binomcxp  44346  wessf1ornlem  45179  projf1o  45191  fsumsermpt  45577  fmuldfeqlem1  45580  fprodcn  45598  sumnnodd  45628  limsupvaluz  45706  limsupvaluz2  45736  supcnvlimsup  45738  supcnvlimsupmpt  45739  liminfval2  45766  liminflelimsuplem  45773  fprodsubrecnncnv  45906  fprodaddrecnncnv  45908  dvsinax  45911  fperdvper  45917  dvcosax  45924  ioodvbdlimc1lem1  45929  ioodvbdlimc1  45931  ioodvbdlimc2  45933  dvnmul  45941  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  dvnprod  45947  itgsin0pilem1  45948  itgiccshift  45978  stoweidlem2  46000  stoweidlem17  46015  stoweidlem32  46030  stoweidlem34  46032  stoweidlem43  46041  stirlinglem2  46073  stirlinglem3  46074  stirlinglem8  46079  dirkerval  46089  dirkerval2  46092  dirkeritg  46100  dirkercncflem3  46103  dirkercncf  46105  fourierdlem14  46119  fourierdlem18  46123  fourierdlem53  46157  fourierdlem62  46166  fourierdlem71  46175  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem80  46184  fourierdlem81  46185  fourierdlem84  46188  fourierdlem88  46192  fourierdlem92  46196  fourierdlem93  46197  fourierdlem94  46198  fourierdlem95  46199  fourierdlem96  46200  fourierdlem97  46201  fourierdlem98  46202  fourierdlem99  46203  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  fourierdlem105  46209  fourierdlem106  46210  fourierdlem107  46211  fourierdlem108  46212  fourierdlem110  46214  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fourierdlem115  46219  fouriersw  46229  elaa2  46232  etransclem1  46233  etransclem5  46237  etransclem6  46238  etransclem11  46243  etransclem13  46245  etransclem41  46273  etransclem47  46279  etransc  46281  ioorrnopn  46303  ioorrnopnxr  46305  subsaliuncl  46356  sge0resplit  46404  sge0fodjrnlem  46414  nnfoctbdj  46454  iundjiun  46458  voliunsge0lem  46470  meaiuninclem  46478  meaiuninc  46479  meaiininclem  46484  meaiininc  46485  omeiunltfirp  46517  carageniuncllem2  46520  carageniuncl  46521  0ome  46527  isomennd  46529  hoicvrrex  46554  ovn0  46564  ovnsubaddlem2  46569  ovnsubadd  46570  sge0hsphoire  46587  hoidmv1lelem3  46591  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hoidmvlelem5  46597  hoidmvle  46598  ovnhoilem2  46600  ovnhoi  46601  hspmbllem2  46625  hspmbl  46627  hoimbl  46629  opnvonmbllem2  46631  ovnsubadd2  46644  ovolval4  46649  ovolval5lem3  46652  ovnovollem3  46656  iccvonmbl  46677  vonioolem2  46679  vonioo  46680  vonicclem2  46682  vonicc  46683  smflimlem4  46772  smfsuplem2  46810  smflimsuplem1  46818  smflimsuplem8  46825  smflimsup  46826  fundcmpsurbijinjpreimafv  47408  prproropf1o  47508  isuspgrim0  47894  cycldlenngric  47928  isubgr3stgrlem8  47972  rmsupp0  48356  domnmsuppn0  48357  rmsuppss  48358  suppmptcfin  48364  ply1mulgsum  48379  lcoc0  48411  linc1  48414  lcoel0  48417  lcoss  48425  el0ldep  48455  lincresunit3  48470  isldepslvec2  48474  itcovalpclem2  48660  itcovalt2lem2  48665  amgmlemALT  49792