Theorem cbvmptv 5204

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 5205 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 2820	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2748	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 633	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5178	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5182	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5182	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2770	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

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

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 2709

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-opab 5163  df-mpt 5182

This theorem is referenced by:  fnmptfvd  6995  mptcnfimad  7940  onnseq  8286  rdgsucmpt2  8371  frsucmpt2  8381  fsetfocdm  8810  fsetprcnex  8811  resixpfo  8886  pw2f1olem  9021  xpmapen  9085  dffi3  9346  ordtypecbv  9434  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  12134  infrenegsup  12137  rpnnen1  12908  caurcvg2  15613  caucvg  15614  summo  15652  zsum  15653  fsum  15655  ackbijnn  15763  cbvprodv  15849  prodmo  15871  zprod  15872  fprod  15876  iprodmul  15938  bpolyval  15984  phimullem  16718  eulerth  16722  iserodd  16775  prmreclem5  16860  prmrec  16862  vdwlem7  16927  vdwlem9  16929  vdwlem10  16930  ramub1  16968  ramcl  16969  yonedalem4c  18212  yonedalem3b  18214  gsumwspan  18783  smndex1iidm  18838  smndex1gid  18840  smndex2dlinvh  18854  grplactcnv  18985  gicqusker  19229  galactghm  19345  symgfixfo  19380  pmtrdifwrdel  19426  pmtrdifwrdel2  19427  odf1o2  19514  sylow1lem2  19540  sylow1  19544  sylow2b  19564  sylow3lem1  19568  sylow3lem5  19572  sylow3  19574  efgtf  19663  efgsval  19672  ghmcyg  19837  cycsubgcyg  19842  ablfaclem3  20030  ablfac2  20032  srgbinomlem4  20176  funcrngcsetcALT  20586  fidomndrnglem  20717  isphld  21621  frlmphl  21748  mplmonmul  22003  evlslem2  22046  mat1ric  22443  mdetralt  22564  smadiadetlem3  22624  pmatcollpw3lem  22739  mp2pm2mplem5  22766  mp2pm2mp  22767  pm2mpmhmlem2  22775  cpmidpmat  22829  cpmadugsumlemF  22832  cpmadugsumfi  22833  cpmadumatpoly  22839  chcoeffeqlem  22841  cayleyhamilton0  22845  cayleyhamilton  22846  cayleyhamiltonALT  22847  cayleyhamilton1  22848  ordtbaslem  23144  ordtbas2  23147  lly1stc  23452  ptpjopn  23568  xkohmeo  23771  fbasrn  23840  elfm  23903  tmdmulg  24048  tmdgsum  24051  qustgpopn  24076  tsmsfbas  24084  tsmsf1o  24101  ustuqtoplem  24195  utopsnneip  24204  fmucnd  24247  ucnextcn  24259  met1stc  24477  prdsxmslem2  24485  metustto  24509  metustexhalf  24512  metuust  24516  cfilucfil2  24517  metuel  24520  metuel2  24521  psmetutop  24523  restmetu  24526  metucn  24527  xrge0tsms  24791  metdsge  24806  expcn  24831  expcnOLD  24833  pi1xfrcnv  25025  minveclem3b  25396  minveclem5  25401  minvec  25404  ovollb2  25458  ovolshftlem2  25479  ovolscalem2  25483  ovolicc  25492  ioombl1  25531  uniioombllem6  25557  volsup2  25574  vitali  25582  mbfi1fseq  25690  mbfmullem  25694  itg2seq  25711  itg2i1fseq  25724  itg2addlem  25727  itg2cnlem1  25730  itg2cn  25732  cbvitgv  25746  dvfsumrlimge0  26005  plyadd  26190  plymul  26191  coeeu  26198  coeid  26211  dvply2g  26260  dvply2gOLD  26261  plydivex  26273  elqaalem2  26296  elqaa  26298  taylthlem1  26349  taylth  26352  pserval  26387  radcnvlem2  26391  radcnvlt2  26396  dvradcnv  26398  pserulm  26399  psercn  26404  pserdvlem2  26406  pserdv  26407  efgh  26518  eff1olem  26525  circgrp  26529  circsubm  26530  logno1  26613  emcl  26981  harmonicbnd  26982  harmonicbnd2  26983  basel  27068  musum  27169  dchr1  27236  dchrptlem2  27244  dchrpt  27246  lgsqrlem4  27328  lgseisenlem3  27356  2sqlem1  27396  dchrmusumlema  27472  dchrmusum2  27473  dchrvmasumlema  27479  dchrvmasumiflem1  27480  dchrisum0ff  27486  dchrisum0lema  27493  dchrisum0lem1b  27494  dchrisum0lem2a  27496  nosupcbv  27682  noinfcbv  27697  precsexlemcbv  28214  seqsfn  28317  seqsp1  28319  wlknwwlksnbij  29973  clwlkclwwlken  30099  clwlknf1oclwwlkn  30171  frgrncvvdeqlem8  30393  frgrncvvdeqlem9  30394  numclwwlk1lem2  30447  ubthlem3  30959  minveco  30971  htth  31005  fsuppcurry1  32813  fsuppcurry2  32814  gsumhashmul  33160  gsummulsubdishift1  33161  gsummulsubdishift1s  33163  gsummulsubdishift2s  33164  xrge0tsmsd  33166  elrgspnlem1  33335  elrgspnlem2  33336  elrgspn  33339  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  elrgspnsubrun  33342  idomsubr  33402  nsgmgc  33504  nsgqusf1olem1  33505  lmicqusker  33510  ricqusker  33519  elrspunidl  33520  elrspunsn  33521  zringfrac  33646  mplvrpmga  33721  mplvrpmrhm  33723  psrgsum  33724  psrmonmul  33726  psrmonprod  33728  splysubrg  33736  issply  33737  esplyfvaln  33750  vietalem  33755  vieta  33756  ply1degltdim  33800  lbsdiflsp0  33803  fedgmullem1  33806  fedgmul  33808  assarrginv  33813  evls1fldgencl  33847  fldextrspunlsplem  33850  fldextrspunlsp  33851  extdgfialglem2  33870  extdgfialg  33871  algextdeglem4  33897  algextdeg  33902  constrcbvlem  33932  madjusmdetlem2  34005  madjusmdet  34008  zartop  34053  zartopon  34054  zart0  34056  zarmxt1  34057  zarcmp  34059  rhmpreimacn  34062  xrge0mulc1cn  34118  xrge0tmd  34122  xrge0tmdALT  34123  cbvesumv  34220  gsumesum  34236  esumlub  34237  esumpcvgval  34255  esumcvg  34263  esumcvg2  34264  eulerpartlems  34537  eulerpart  34559  fibp1  34578  rrvadd  34629  ballotlemfval  34667  ballotlemi  34678  ballotlemsval  34686  ballotlemsv  34687  ballotlemsf1o  34691  ballotlemrval  34695  ballotlemrinv  34711  signsply0  34728  actfunsnf1o  34781  actfunsnrndisj  34782  itgexpif  34783  hgt750lemb  34833  onvf1odlem3  35318  derangfmla  35403  erdsze  35415  pconnpi1  35450  cvmscbv  35471  cvmsss2  35487  cvmliftlem15  35511  cvmlift2  35529  cvmlift3  35541  elmrsubrn  35733  iprodefisum  35954  cbvprodvw2  36460  cbvitgvw2  36461  knoppcnlem7  36718  knoppf  36754  f1omptsn  37586  mptsnun  37588  fin2so  37852  poimirlem27  37892  broucube  37899  ftc1anclem5  37942  ftc1anclem6  37943  sdclem2  37987  prdstotbnd  38039  prdsbnd2  38040  heiborlem10  38065  lshpkrcl  39486  tendoplcbv  41145  tendo0cbv  41156  tendoicbv  41163  lcfl7N  41871  lcf1o  41921  hdmap1cbv  42172  frlmsnic  42904  evlselv  42939  mzpclval  43076  mzpcompact2lem  43102  rmxyval  43266  dnnumch1  43395  aomclem3  43407  aomclem8  43412  dfac21  43417  pwfi2f1o  43447  dftrcl3  44070  dfrtrcl3  44083  rfovcnvf1od  44354  fsovrfovd  44359  fsovcnvlem  44363  dssmapnvod  44370  clsk3nimkb  44390  radcnvrat  44664  expgrowthi  44683  expgrowth  44685  dvradcnv2  44697  binomcxplemradcnv  44702  binomcxplemdvbinom  44703  binomcxplemdvsum  44705  binomcxplemnotnn0  44706  binomcxp  44707  wessf1ornlem  45538  projf1o  45549  fsumsermpt  45933  fmuldfeqlem1  45936  fprodcn  45954  sumnnodd  45984  limsupvaluz  46060  limsupvaluz2  46090  supcnvlimsup  46092  supcnvlimsupmpt  46093  liminfval2  46120  liminflelimsuplem  46127  fprodsubrecnncnv  46260  fprodaddrecnncnv  46262  dvsinax  46265  fperdvper  46271  dvcosax  46278  ioodvbdlimc1lem1  46283  ioodvbdlimc1  46285  ioodvbdlimc2  46287  dvnmul  46295  dvnprodlem1  46298  dvnprodlem2  46299  dvnprodlem3  46300  dvnprod  46301  itgsin0pilem1  46302  itgiccshift  46332  stoweidlem2  46354  stoweidlem17  46369  stoweidlem32  46384  stoweidlem34  46386  stoweidlem43  46395  stirlinglem2  46427  stirlinglem3  46428  stirlinglem8  46433  dirkerval  46443  dirkerval2  46446  dirkeritg  46454  dirkercncflem3  46457  dirkercncf  46459  fourierdlem14  46473  fourierdlem18  46477  fourierdlem53  46511  fourierdlem62  46520  fourierdlem71  46529  fourierdlem74  46532  fourierdlem75  46533  fourierdlem76  46534  fourierdlem80  46538  fourierdlem81  46539  fourierdlem84  46542  fourierdlem88  46546  fourierdlem92  46550  fourierdlem93  46551  fourierdlem94  46552  fourierdlem95  46553  fourierdlem96  46554  fourierdlem97  46555  fourierdlem98  46556  fourierdlem99  46557  fourierdlem101  46559  fourierdlem103  46561  fourierdlem104  46562  fourierdlem105  46563  fourierdlem106  46564  fourierdlem107  46565  fourierdlem108  46566  fourierdlem110  46568  fourierdlem111  46569  fourierdlem112  46570  fourierdlem113  46571  fourierdlem115  46573  fouriersw  46583  elaa2  46586  etransclem1  46587  etransclem5  46591  etransclem6  46592  etransclem11  46597  etransclem13  46599  etransclem41  46627  etransclem47  46633  etransc  46635  ioorrnopn  46657  ioorrnopnxr  46659  subsaliuncl  46710  sge0resplit  46758  sge0fodjrnlem  46768  nnfoctbdj  46808  iundjiun  46812  voliunsge0lem  46824  meaiuninclem  46832  meaiuninc  46833  meaiininclem  46838  meaiininc  46839  omeiunltfirp  46871  carageniuncllem2  46874  carageniuncl  46875  0ome  46881  isomennd  46883  hoicvrrex  46908  ovn0  46918  ovnsubaddlem2  46923  ovnsubadd  46924  sge0hsphoire  46941  hoidmv1lelem3  46945  hoidmv1le  46946  hoidmvlelem1  46947  hoidmvlelem2  46948  hoidmvlelem3  46949  hoidmvlelem4  46950  hoidmvlelem5  46951  hoidmvle  46952  ovnhoilem2  46954  ovnhoi  46955  hspmbllem2  46979  hspmbl  46981  hoimbl  46983  opnvonmbllem2  46985  ovnsubadd2  46998  ovolval4  47003  ovolval5lem3  47006  ovnovollem3  47010  iccvonmbl  47031  vonioolem2  47033  vonioo  47034  vonicclem2  47036  vonicc  47037  smflimlem4  47126  smfsuplem2  47164  smflimsuplem1  47172  smflimsuplem8  47179  smflimsup  47180  fundcmpsurbijinjpreimafv  47761  prproropf1o  47861  isuspgrim0  48248  cycldlenngric  48282  isubgr3stgrlem8  48327  rmsupp0  48722  domnmsuppn0  48723  rmsuppss  48724  suppmptcfin  48730  ply1mulgsum  48744  lcoc0  48776  linc1  48779  lcoel0  48782  lcoss  48790  el0ldep  48820  lincresunit3  48835  isldepslvec2  48839  itcovalpclem2  49025  itcovalt2lem2  49030  amgmlemALT  50156