Theorem cbvmptv 5197

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 5198 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 2816	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2744	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5171	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5175	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5175	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2766	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {copab 5155   ↦ cmpt 5174

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-opab 5156  df-mpt 5175

This theorem is referenced by:  fnmptfvd  6980  mptcnfimad  7924  onnseq  8270  rdgsucmpt2  8355  frsucmpt2  8365  fsetfocdm  8791  fsetprcnex  8792  resixpfo  8866  pw2f1olem  9001  xpmapen  9065  dffi3  9322  ordtypecbv  9410  inf3lema  9521  cantnflem1  9586  cnfcomlem  9596  infxpenc2  9920  fseqenlem1  9922  dfac8a  9928  dfac12r  10045  r1om  10141  fictb  10142  cfsmo  10169  coftr  10171  fin23lem38  10247  compsscnv  10269  isf34lem1  10270  compss  10274  fin1a2lem1  10298  fin1a2lem3  10300  fin1a2lem13  10310  itunisuc  10317  hsmex  10330  domtriom  10341  axdc2  10347  zorn2g  10401  ttukey2g  10414  axdc  10419  konigth  10467  pwcfsdom  10481  canthp1  10552  wunex2  10636  wuncval2  10645  negiso  12109  infrenegsup  12112  rpnnen1  12883  caurcvg2  15587  caucvg  15588  summo  15626  zsum  15627  fsum  15629  ackbijnn  15737  cbvprodv  15823  prodmo  15845  zprod  15846  fprod  15850  iprodmul  15912  bpolyval  15958  phimullem  16692  eulerth  16696  iserodd  16749  prmreclem5  16834  prmrec  16836  vdwlem7  16901  vdwlem9  16903  vdwlem10  16904  ramub1  16942  ramcl  16943  yonedalem4c  18185  yonedalem3b  18187  gsumwspan  18756  smndex1iidm  18811  smndex1gid  18813  smndex2dlinvh  18827  grplactcnv  18958  gicqusker  19202  galactghm  19318  symgfixfo  19353  pmtrdifwrdel  19399  pmtrdifwrdel2  19400  odf1o2  19487  sylow1lem2  19513  sylow1  19517  sylow2b  19537  sylow3lem1  19541  sylow3lem5  19545  sylow3  19547  efgtf  19636  efgsval  19645  ghmcyg  19810  cycsubgcyg  19815  ablfaclem3  20003  ablfac2  20005  srgbinomlem4  20149  funcrngcsetcALT  20558  fidomndrnglem  20689  isphld  21593  frlmphl  21720  mplmonmul  21972  evlslem2  22015  mat1ric  22403  mdetralt  22524  smadiadetlem3  22584  pmatcollpw3lem  22699  mp2pm2mplem5  22726  mp2pm2mp  22727  pm2mpmhmlem2  22735  cpmidpmat  22789  cpmadugsumlemF  22792  cpmadugsumfi  22793  cpmadumatpoly  22799  chcoeffeqlem  22801  cayleyhamilton0  22805  cayleyhamilton  22806  cayleyhamiltonALT  22807  cayleyhamilton1  22808  ordtbaslem  23104  ordtbas2  23107  lly1stc  23412  ptpjopn  23528  xkohmeo  23731  fbasrn  23800  elfm  23863  tmdmulg  24008  tmdgsum  24011  qustgpopn  24036  tsmsfbas  24044  tsmsf1o  24061  ustuqtoplem  24155  utopsnneip  24164  fmucnd  24207  ucnextcn  24219  met1stc  24437  prdsxmslem2  24445  metustto  24469  metustexhalf  24472  metuust  24476  cfilucfil2  24477  metuel  24480  metuel2  24481  psmetutop  24483  restmetu  24486  metucn  24487  xrge0tsms  24751  metdsge  24766  expcn  24791  expcnOLD  24793  pi1xfrcnv  24985  minveclem3b  25356  minveclem5  25361  minvec  25364  ovollb2  25418  ovolshftlem2  25439  ovolscalem2  25443  ovolicc  25452  ioombl1  25491  uniioombllem6  25517  volsup2  25534  vitali  25542  mbfi1fseq  25650  mbfmullem  25654  itg2seq  25671  itg2i1fseq  25684  itg2addlem  25687  itg2cnlem1  25690  itg2cn  25692  cbvitgv  25706  dvfsumrlimge0  25965  plyadd  26150  plymul  26151  coeeu  26158  coeid  26171  dvply2g  26220  dvply2gOLD  26221  plydivex  26233  elqaalem2  26256  elqaa  26258  taylthlem1  26309  taylth  26312  pserval  26347  radcnvlem2  26351  radcnvlt2  26356  dvradcnv  26358  pserulm  26359  psercn  26364  pserdvlem2  26366  pserdv  26367  efgh  26478  eff1olem  26485  circgrp  26489  circsubm  26490  logno1  26573  emcl  26941  harmonicbnd  26942  harmonicbnd2  26943  basel  27028  musum  27129  dchr1  27196  dchrptlem2  27204  dchrpt  27206  lgsqrlem4  27288  lgseisenlem3  27316  2sqlem1  27356  dchrmusumlema  27432  dchrmusum2  27433  dchrvmasumlema  27439  dchrvmasumiflem1  27440  dchrisum0ff  27446  dchrisum0lema  27453  dchrisum0lem1b  27454  dchrisum0lem2a  27456  nosupcbv  27642  noinfcbv  27657  precsexlemcbv  28145  seqsfn  28240  seqsp1  28242  wlknwwlksnbij  29868  clwlkclwwlken  29994  clwlknf1oclwwlkn  30066  frgrncvvdeqlem8  30288  frgrncvvdeqlem9  30289  numclwwlk1lem2  30342  ubthlem3  30854  minveco  30866  htth  30900  fsuppcurry1  32711  fsuppcurry2  32712  gsumhashmul  33048  xrge0tsmsd  33049  elrgspnlem1  33216  elrgspnlem2  33217  elrgspn  33220  elrgspnsubrunlem1  33221  elrgspnsubrunlem2  33222  elrgspnsubrun  33223  idomsubr  33282  nsgmgc  33384  nsgqusf1olem1  33385  lmicqusker  33390  ricqusker  33399  elrspunidl  33400  elrspunsn  33401  zringfrac  33526  mplvrpmga  33593  mplvrpmrhm  33595  splysubrg  33601  issply  33602  ply1degltdim  33657  lbsdiflsp0  33660  fedgmullem1  33663  fedgmul  33665  assarrginv  33670  evls1fldgencl  33704  fldextrspunlsplem  33707  fldextrspunlsp  33708  extdgfialglem2  33727  extdgfialg  33728  algextdeglem4  33754  algextdeg  33759  constrcbvlem  33789  madjusmdetlem2  33862  madjusmdet  33865  zartop  33910  zartopon  33911  zart0  33913  zarmxt1  33914  zarcmp  33916  rhmpreimacn  33919  xrge0mulc1cn  33975  xrge0tmd  33979  xrge0tmdALT  33980  cbvesumv  34077  gsumesum  34093  esumlub  34094  esumpcvgval  34112  esumcvg  34120  esumcvg2  34121  eulerpartlems  34394  eulerpart  34416  fibp1  34435  rrvadd  34486  ballotlemfval  34524  ballotlemi  34535  ballotlemsval  34543  ballotlemsv  34544  ballotlemsf1o  34548  ballotlemrval  34552  ballotlemrinv  34568  signsply0  34585  actfunsnf1o  34638  actfunsnrndisj  34639  itgexpif  34640  hgt750lemb  34690  onvf1odlem3  35170  derangfmla  35255  erdsze  35267  pconnpi1  35302  cvmscbv  35323  cvmsss2  35339  cvmliftlem15  35363  cvmlift2  35381  cvmlift3  35393  elmrsubrn  35585  iprodefisum  35806  cbvprodvw2  36312  cbvitgvw2  36313  knoppcnlem7  36564  knoppf  36600  f1omptsn  37402  mptsnun  37404  fin2so  37667  poimirlem27  37707  broucube  37714  ftc1anclem5  37757  ftc1anclem6  37758  sdclem2  37802  prdstotbnd  37854  prdsbnd2  37855  heiborlem10  37880  lshpkrcl  39235  tendoplcbv  40894  tendo0cbv  40905  tendoicbv  40912  lcfl7N  41620  lcf1o  41670  hdmap1cbv  41921  frlmsnic  42658  evlselv  42705  mzpclval  42842  mzpcompact2lem  42868  rmxyval  43032  dnnumch1  43161  aomclem3  43173  aomclem8  43178  dfac21  43183  pwfi2f1o  43213  dftrcl3  43837  dfrtrcl3  43850  rfovcnvf1od  44121  fsovrfovd  44126  fsovcnvlem  44130  dssmapnvod  44137  clsk3nimkb  44157  radcnvrat  44431  expgrowthi  44450  expgrowth  44452  dvradcnv2  44464  binomcxplemradcnv  44469  binomcxplemdvbinom  44470  binomcxplemdvsum  44472  binomcxplemnotnn0  44473  binomcxp  44474  wessf1ornlem  45306  projf1o  45318  fsumsermpt  45703  fmuldfeqlem1  45706  fprodcn  45724  sumnnodd  45754  limsupvaluz  45830  limsupvaluz2  45860  supcnvlimsup  45862  supcnvlimsupmpt  45863  liminfval2  45890  liminflelimsuplem  45897  fprodsubrecnncnv  46030  fprodaddrecnncnv  46032  dvsinax  46035  fperdvper  46041  dvcosax  46048  ioodvbdlimc1lem1  46053  ioodvbdlimc1  46055  ioodvbdlimc2  46057  dvnmul  46065  dvnprodlem1  46068  dvnprodlem2  46069  dvnprodlem3  46070  dvnprod  46071  itgsin0pilem1  46072  itgiccshift  46102  stoweidlem2  46124  stoweidlem17  46139  stoweidlem32  46154  stoweidlem34  46156  stoweidlem43  46165  stirlinglem2  46197  stirlinglem3  46198  stirlinglem8  46203  dirkerval  46213  dirkerval2  46216  dirkeritg  46224  dirkercncflem3  46227  dirkercncf  46229  fourierdlem14  46243  fourierdlem18  46247  fourierdlem53  46281  fourierdlem62  46290  fourierdlem71  46299  fourierdlem74  46302  fourierdlem75  46303  fourierdlem76  46304  fourierdlem80  46308  fourierdlem81  46309  fourierdlem84  46312  fourierdlem88  46316  fourierdlem92  46320  fourierdlem93  46321  fourierdlem94  46322  fourierdlem95  46323  fourierdlem96  46324  fourierdlem97  46325  fourierdlem98  46326  fourierdlem99  46327  fourierdlem101  46329  fourierdlem103  46331  fourierdlem104  46332  fourierdlem105  46333  fourierdlem106  46334  fourierdlem107  46335  fourierdlem108  46336  fourierdlem110  46338  fourierdlem111  46339  fourierdlem112  46340  fourierdlem113  46341  fourierdlem115  46343  fouriersw  46353  elaa2  46356  etransclem1  46357  etransclem5  46361  etransclem6  46362  etransclem11  46367  etransclem13  46369  etransclem41  46397  etransclem47  46403  etransc  46405  ioorrnopn  46427  ioorrnopnxr  46429  subsaliuncl  46480  sge0resplit  46528  sge0fodjrnlem  46538  nnfoctbdj  46578  iundjiun  46582  voliunsge0lem  46594  meaiuninclem  46602  meaiuninc  46603  meaiininclem  46608  meaiininc  46609  omeiunltfirp  46641  carageniuncllem2  46644  carageniuncl  46645  0ome  46651  isomennd  46653  hoicvrrex  46678  ovn0  46688  ovnsubaddlem2  46693  ovnsubadd  46694  sge0hsphoire  46711  hoidmv1lelem3  46715  hoidmv1le  46716  hoidmvlelem1  46717  hoidmvlelem2  46718  hoidmvlelem3  46719  hoidmvlelem4  46720  hoidmvlelem5  46721  hoidmvle  46722  ovnhoilem2  46724  ovnhoi  46725  hspmbllem2  46749  hspmbl  46751  hoimbl  46753  opnvonmbllem2  46755  ovnsubadd2  46768  ovolval4  46773  ovolval5lem3  46776  ovnovollem3  46780  iccvonmbl  46801  vonioolem2  46803  vonioo  46804  vonicclem2  46806  vonicc  46807  smflimlem4  46896  smfsuplem2  46934  smflimsuplem1  46942  smflimsuplem8  46949  smflimsup  46950  fundcmpsurbijinjpreimafv  47531  prproropf1o  47631  isuspgrim0  48018  cycldlenngric  48052  isubgr3stgrlem8  48097  rmsupp0  48492  domnmsuppn0  48493  rmsuppss  48494  suppmptcfin  48500  ply1mulgsum  48515  lcoc0  48547  linc1  48550  lcoel0  48553  lcoss  48561  el0ldep  48591  lincresunit3  48606  isldepslvec2  48610  itcovalpclem2  48796  itcovalt2lem2  48801  amgmlemALT  49928