Theorem mpteq2ia 5207

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.) (Proof shortened by SN, 11-Nov-2024.)

Hypothesis

Ref	Expression
mpteq2ia.1	⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)

Assertion

Ref	Expression
mpteq2ia	⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Proof of Theorem mpteq2ia

Step	Hyp	Ref	Expression
1		mpteq2ia.1	. . . 4 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
2	1	adantl 486	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5205	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
4	3	mptru 1574	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4   = wceq 1567  ⊤wtru 1568   ∈ wcel 2149   ↦ cmpt 5193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-opab 5175  df-mpt 5194

This theorem is referenced by:  mpteq2i  5208  partfun  6680  feqresmpt  6948  elfvmptrab  7017  fmptap  7166  offres  7976  resixpfo  8930  dfoi  9469  cantnflem1d  9653  cantnflem1  9654  dfceil2  13868  dfid5  15060  dfid6  15061  cnrecnv  15212  ackbijnn  15878  harmonic  15909  ege2le3  16140  eirrlem  16256  prmrec  16978  imasdsval2  17566  dfinito2  18056  dftermo2  18057  dfinito3  18058  dftermo3  18059  smndex1iidm  18956  smndex2dlinvh  18975  cayleylem1  19478  pmtrprfval  19553  gsumzsplit  19993  gsum2dlem2  20037  dmdprdsplitlem  20105  frlmip  21893  coe1sclmul  22408  coe1sclmul2  22410  mdetunilem9  22742  leordtvallem1  23332  leordtvallem2  23333  txkgen  23774  cnmpt1st  23790  cnmpt2nd  23791  tmdgsum  24217  tsmssplit  24274  cnfldnm  24900  expcn  24996  pcorev2  25152  pi1xfrcnv  25181  rrxip  25514  mbfi1flim  25847  itg2uba  25867  itg2cnlem1  25885  itg2cnlem2  25886  itgitg2  25931  itgss3  25939  itgless  25941  ibladdlem  25944  itgaddlem1  25947  iblabslem  25952  itggt0  25968  itgcn  25969  limcdif  26000  limcres  26010  cnplimc  26011  dvcobr  26070  dvexp  26077  dveflem  26103  dvef  26104  dvlip  26117  dvlipcn  26118  lhop  26140  tdeglem2  26183  plyid  26331  coeidp  26385  dgrid  26386  plymulidp  26408  pserdvlem2  26553  abelth  26566  dvrelog  26764  logcn  26774  dvlog  26778  advlog  26781  advlogexp  26782  logtayl  26787  logccv  26790  dvcxp1  26867  dvsqrt  26869  dvcncxp1  26870  dvcnsqrt  26871  resqrtcn  26876  loglesqrt  26888  logblog  26919  dvatan  27062  leibpilem2  27068  leibpi  27069  efrlim  27096  sqrtlim  27099  amgmlem  27116  emcllem5  27126  lgamgulmlem2  27156  lgam1  27190  chtublem  27337  logfacrlim2  27352  bposlem6  27415  chto1lb  27604  vmadivsum  27608  dchrvmasumlema  27626  mulogsumlem  27657  logdivsum  27659  logsqvma2  27669  log2sumbnd  27670  selberglem1  27671  selberglem3  27673  selberg  27674  selberg2lem  27676  selberg2  27677  pntrmax  27690  pntrsumo1  27691  selbergr  27694  selbergs  27700  pnt2  27739  pnt  27740  ostth2  27763  ostth  27765  hilnormi  31452  bra0  32239  partfun2  32958  mplmonprod  33885  zrhre  34350  qqhre  34351  eulerpartgbij  34703  elmrsubrn  35907  faclim  36133  ptrest  38153  poimirlem19  38173  poimirlem20  38174  poimirlem30  38184  ovoliunnfl  38196  voliunnfl  38198  mbfposadd  38201  dvtan  38204  itg2addnclem  38205  ibladdnclem  38210  itgaddnclem1  38212  iblabsnclem  38217  itggt0cn  38224  ftc1anclem4  38230  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anclem8  38234  dvasin  38238  dvacos  38239  areacirclem1  38242  dfadjliftmap2  38991  dfblockliftmap2  38995  aks6d1c1p5  42764  redvmptabs  43006  readvrec2  43007  readvrec  43008  readvcot  43010  arearect  43829  areaquad  43830  cantnfresb  43938  mptrcllem  44226  dfrcl2  44287  dfrcl3  44288  dftrcl3  44333  dfrtrcl3  44346  dfrtrcl4  44351  lhe4.4ex1a  44926  binomcxplemrat  44947  rnsnf  45789  feqresmptf  45833  limsupresre  46297  limsupvaluzmpt  46318  limsup10ex  46374  liminf10ex  46375  dvnprodlem1  46547  itgsin0pilem1  46551  wallispilem4  46669  wallispi2  46674  stirlinglem1  46675  stirlinglem3  46677  dirkercncflem2  46705  fourierdlem48  46755  fourierdlem49  46756  fourierdlem56  46763  fourierdlem57  46764  fourierdlem58  46765  fourierdlem62  46769  fourierdlem107  46814  fouriersw  46832  etransclem46  46881  sge0tsms  46981  sge0less  46993  sge0iun  47020  meadjun  47063  ovn02  47169  hoidmv1le  47195  hspmbllem2  47228  smflimsuplem3  47423  indprm  48265  indprmfz  48266  ackval1  49341  ackval2  49342  ackval3  49343  dftermo4  50160