Theorem cbvmptv 5214

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 5215 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 2812	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvmptv.1	. . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶)
3	2	eqeq2d 2741	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶))
4	1, 3	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)))
5	4	cbvopab1v 5188	. 2 ⊢ {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
6		df-mpt 5192	. 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑧⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)}
7		df-mpt 5192	. 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {⟨𝑦, 𝑧⟩ ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)}
8	5, 6, 7	3eqtr4i 2763	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶)

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

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-opab 5173  df-mpt 5192

This theorem is referenced by:  fnmptfvd  7016  mptcnfimad  7968  onnseq  8316  rdgsucmpt2  8401  frsucmpt2  8411  fsetfocdm  8837  fsetprcnex  8838  resixpfo  8912  pw2f1olem  9050  xpmapen  9115  dffi3  9389  ordtypecbv  9477  inf3lema  9584  cantnflem1  9649  cnfcomlem  9659  infxpenc2  9982  fseqenlem1  9984  dfac8a  9990  dfac12r  10107  r1om  10203  fictb  10204  cfsmo  10231  coftr  10233  fin23lem38  10309  compsscnv  10331  isf34lem1  10332  compss  10336  fin1a2lem1  10360  fin1a2lem3  10362  fin1a2lem13  10372  itunisuc  10379  hsmex  10392  domtriom  10403  axdc2  10409  zorn2g  10463  ttukey2g  10476  axdc  10481  konigth  10529  pwcfsdom  10543  canthp1  10614  wunex2  10698  wuncval2  10707  negiso  12170  infrenegsup  12173  rpnnen1  12949  caurcvg2  15651  caucvg  15652  summo  15690  zsum  15691  fsum  15693  ackbijnn  15801  cbvprodv  15887  prodmo  15909  zprod  15910  fprod  15914  iprodmul  15976  bpolyval  16022  phimullem  16756  eulerth  16760  iserodd  16813  prmreclem5  16898  prmrec  16900  vdwlem7  16965  vdwlem9  16967  vdwlem10  16968  ramub1  17006  ramcl  17007  yonedalem4c  18245  yonedalem3b  18247  gsumwspan  18780  smndex1iidm  18835  smndex1gid  18837  smndex2dlinvh  18851  grplactcnv  18982  gicqusker  19227  galactghm  19341  symgfixfo  19376  pmtrdifwrdel  19422  pmtrdifwrdel2  19423  odf1o2  19510  sylow1lem2  19536  sylow1  19540  sylow2b  19560  sylow3lem1  19564  sylow3lem5  19568  sylow3  19570  efgtf  19659  efgsval  19668  ghmcyg  19833  cycsubgcyg  19838  ablfaclem3  20026  ablfac2  20028  srgbinomlem4  20145  funcrngcsetcALT  20557  fidomndrnglem  20688  isphld  21570  frlmphl  21697  mplmonmul  21950  evlslem2  21993  mat1ric  22381  mdetralt  22502  smadiadetlem3  22562  pmatcollpw3lem  22677  mp2pm2mplem5  22704  mp2pm2mp  22705  pm2mpmhmlem2  22713  cpmidpmat  22767  cpmadugsumlemF  22770  cpmadugsumfi  22771  cpmadumatpoly  22777  chcoeffeqlem  22779  cayleyhamilton0  22783  cayleyhamilton  22784  cayleyhamiltonALT  22785  cayleyhamilton1  22786  ordtbaslem  23082  ordtbas2  23085  lly1stc  23390  ptpjopn  23506  xkohmeo  23709  fbasrn  23778  elfm  23841  tmdmulg  23986  tmdgsum  23989  qustgpopn  24014  tsmsfbas  24022  tsmsf1o  24039  ustuqtoplem  24134  utopsnneip  24143  fmucnd  24186  ucnextcn  24198  met1stc  24416  prdsxmslem2  24424  metustto  24448  metustexhalf  24451  metuust  24455  cfilucfil2  24456  metuel  24459  metuel2  24460  psmetutop  24462  restmetu  24465  metucn  24466  xrge0tsms  24730  metdsge  24745  expcn  24770  expcnOLD  24772  pi1xfrcnv  24964  minveclem3b  25335  minveclem5  25340  minvec  25343  ovollb2  25397  ovolshftlem2  25418  ovolscalem2  25422  ovolicc  25431  ioombl1  25470  uniioombllem6  25496  volsup2  25513  vitali  25521  mbfi1fseq  25629  mbfmullem  25633  itg2seq  25650  itg2i1fseq  25663  itg2addlem  25666  itg2cnlem1  25669  itg2cn  25671  cbvitgv  25685  dvfsumrlimge0  25944  plyadd  26129  plymul  26130  coeeu  26137  coeid  26150  dvply2g  26199  dvply2gOLD  26200  plydivex  26212  elqaalem2  26235  elqaa  26237  taylthlem1  26288  taylth  26291  pserval  26326  radcnvlem2  26330  radcnvlt2  26335  dvradcnv  26337  pserulm  26338  psercn  26343  pserdvlem2  26345  pserdv  26346  efgh  26457  eff1olem  26464  circgrp  26468  circsubm  26469  logno1  26552  emcl  26920  harmonicbnd  26921  harmonicbnd2  26922  basel  27007  musum  27108  dchr1  27175  dchrptlem2  27183  dchrpt  27185  lgsqrlem4  27267  lgseisenlem3  27295  2sqlem1  27335  dchrmusumlema  27411  dchrmusum2  27412  dchrvmasumlema  27418  dchrvmasumiflem1  27419  dchrisum0ff  27425  dchrisum0lema  27432  dchrisum0lem1b  27433  dchrisum0lem2a  27435  nosupcbv  27621  noinfcbv  27636  precsexlemcbv  28115  seqsfn  28210  seqsp1  28212  wlknwwlksnbij  29825  clwlkclwwlken  29948  clwlknf1oclwwlkn  30020  frgrncvvdeqlem8  30242  frgrncvvdeqlem9  30243  numclwwlk1lem2  30296  ubthlem3  30808  minveco  30820  htth  30854  fsuppcurry1  32655  fsuppcurry2  32656  gsumhashmul  33008  xrge0tsmsd  33009  elrgspnlem1  33200  elrgspnlem2  33201  elrgspn  33204  elrgspnsubrunlem1  33205  elrgspnsubrunlem2  33206  elrgspnsubrun  33207  idomsubr  33266  nsgmgc  33390  nsgqusf1olem1  33391  lmicqusker  33396  ricqusker  33405  elrspunidl  33406  elrspunsn  33407  zringfrac  33532  ply1degltdim  33626  lbsdiflsp0  33629  fedgmullem1  33632  fedgmul  33634  assarrginv  33639  evls1fldgencl  33672  fldextrspunlsplem  33675  fldextrspunlsp  33676  algextdeglem4  33717  algextdeg  33722  constrcbvlem  33752  madjusmdetlem2  33825  madjusmdet  33828  zartop  33873  zartopon  33874  zart0  33876  zarmxt1  33877  zarcmp  33879  rhmpreimacn  33882  xrge0mulc1cn  33938  xrge0tmd  33942  xrge0tmdALT  33943  cbvesumv  34040  gsumesum  34056  esumlub  34057  esumpcvgval  34075  esumcvg  34083  esumcvg2  34084  eulerpartlems  34358  eulerpart  34380  fibp1  34399  rrvadd  34450  ballotlemfval  34488  ballotlemi  34499  ballotlemsval  34507  ballotlemsv  34508  ballotlemsf1o  34512  ballotlemrval  34516  ballotlemrinv  34532  signsply0  34549  actfunsnf1o  34602  actfunsnrndisj  34603  itgexpif  34604  hgt750lemb  34654  onvf1odlem3  35099  derangfmla  35184  erdsze  35196  pconnpi1  35231  cvmscbv  35252  cvmsss2  35268  cvmliftlem15  35292  cvmlift2  35310  cvmlift3  35322  elmrsubrn  35514  iprodefisum  35735  cbvprodvw2  36242  cbvitgvw2  36243  knoppcnlem7  36494  knoppf  36530  f1omptsn  37332  mptsnun  37334  fin2so  37608  poimirlem27  37648  broucube  37655  ftc1anclem5  37698  ftc1anclem6  37699  sdclem2  37743  prdstotbnd  37795  prdsbnd2  37796  heiborlem10  37821  lshpkrcl  39116  tendoplcbv  40776  tendo0cbv  40787  tendoicbv  40794  lcfl7N  41502  lcf1o  41552  hdmap1cbv  41803  frlmsnic  42535  evlselv  42582  mzpclval  42720  mzpcompact2lem  42746  rmxyval  42911  dnnumch1  43040  aomclem3  43052  aomclem8  43057  dfac21  43062  pwfi2f1o  43092  dftrcl3  43716  dfrtrcl3  43729  rfovcnvf1od  44000  fsovrfovd  44005  fsovcnvlem  44009  dssmapnvod  44016  clsk3nimkb  44036  radcnvrat  44310  expgrowthi  44329  expgrowth  44331  dvradcnv2  44343  binomcxplemradcnv  44348  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  binomcxp  44353  wessf1ornlem  45186  projf1o  45198  fsumsermpt  45584  fmuldfeqlem1  45587  fprodcn  45605  sumnnodd  45635  limsupvaluz  45713  limsupvaluz2  45743  supcnvlimsup  45745  supcnvlimsupmpt  45746  liminfval2  45773  liminflelimsuplem  45780  fprodsubrecnncnv  45913  fprodaddrecnncnv  45915  dvsinax  45918  fperdvper  45924  dvcosax  45931  ioodvbdlimc1lem1  45936  ioodvbdlimc1  45938  ioodvbdlimc2  45940  dvnmul  45948  dvnprodlem1  45951  dvnprodlem2  45952  dvnprodlem3  45953  dvnprod  45954  itgsin0pilem1  45955  itgiccshift  45985  stoweidlem2  46007  stoweidlem17  46022  stoweidlem32  46037  stoweidlem34  46039  stoweidlem43  46048  stirlinglem2  46080  stirlinglem3  46081  stirlinglem8  46086  dirkerval  46096  dirkerval2  46099  dirkeritg  46107  dirkercncflem3  46110  dirkercncf  46112  fourierdlem14  46126  fourierdlem18  46130  fourierdlem53  46164  fourierdlem62  46173  fourierdlem71  46182  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem80  46191  fourierdlem81  46192  fourierdlem84  46195  fourierdlem88  46199  fourierdlem92  46203  fourierdlem93  46204  fourierdlem94  46205  fourierdlem95  46206  fourierdlem96  46207  fourierdlem97  46208  fourierdlem98  46209  fourierdlem99  46210  fourierdlem101  46212  fourierdlem103  46214  fourierdlem104  46215  fourierdlem105  46216  fourierdlem106  46217  fourierdlem107  46218  fourierdlem108  46219  fourierdlem110  46221  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fourierdlem115  46226  fouriersw  46236  elaa2  46239  etransclem1  46240  etransclem5  46244  etransclem6  46245  etransclem11  46250  etransclem13  46252  etransclem41  46280  etransclem47  46286  etransc  46288  ioorrnopn  46310  ioorrnopnxr  46312  subsaliuncl  46363  sge0resplit  46411  sge0fodjrnlem  46421  nnfoctbdj  46461  iundjiun  46465  voliunsge0lem  46477  meaiuninclem  46485  meaiuninc  46486  meaiininclem  46491  meaiininc  46492  omeiunltfirp  46524  carageniuncllem2  46527  carageniuncl  46528  0ome  46534  isomennd  46536  hoicvrrex  46561  ovn0  46571  ovnsubaddlem2  46576  ovnsubadd  46577  sge0hsphoire  46594  hoidmv1lelem3  46598  hoidmv1le  46599  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  hoidmvlelem5  46604  hoidmvle  46605  ovnhoilem2  46607  ovnhoi  46608  hspmbllem2  46632  hspmbl  46634  hoimbl  46636  opnvonmbllem2  46638  ovnsubadd2  46651  ovolval4  46656  ovolval5lem3  46659  ovnovollem3  46663  iccvonmbl  46684  vonioolem2  46686  vonioo  46687  vonicclem2  46689  vonicc  46690  smflimlem4  46779  smfsuplem2  46817  smflimsuplem1  46825  smflimsuplem8  46832  smflimsup  46833  fundcmpsurbijinjpreimafv  47412  prproropf1o  47512  isuspgrim0  47898  cycldlenngric  47932  isubgr3stgrlem8  47976  rmsupp0  48360  domnmsuppn0  48361  rmsuppss  48362  suppmptcfin  48368  ply1mulgsum  48383  lcoc0  48415  linc1  48418  lcoel0  48421  lcoss  48429  el0ldep  48459  lincresunit3  48474  isldepslvec2  48478  itcovalpclem2  48664  itcovalt2lem2  48669  amgmlemALT  49796