Theorem mpteq2ia 5199

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 487	. . 3 ⊢ ((⊤ ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐶)
3	2	mpteq2dva 5197	. 2 ⊢ (⊤ → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
4	3	mptru 1576	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ⊤wtru 1570   ∈ wcel 2144   ↦ cmpt 5185

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-opab 5167  df-mpt 5186

This theorem is used by:  mpteq2i  5200  partfun  6687  feqresmpt  6955  elfvmptrab  7024  fmptap  7176  offres  7996  resixpfo  8968  dfoi  9509  cantnflem1d  9693  cantnflem1  9694  dfceil2  13983  dfid5  15186  dfid6  15187  cnrecnv  15338  ackbijnn  16003  harmonic  16034  ege2le3  16262  eirrlem  16378  prmrec  17106  imasdsval2  17694  dfinito2  18184  dftermo2  18185  dfinito3  18186  dftermo3  18187  smndex1iidm  19103  smndex2dlinvh  19122  cayleylem1  19632  pmtrprfval  19707  gsumzsplit  20147  gsum2dlem2  20191  dmdprdsplitlem  20259  frlmip  22090  coe1sclmul  22607  coe1sclmul2  22609  mdetunilem9  22941  leordtvallem1  23534  leordtvallem2  23535  txkgen  23977  cnmpt1st  23993  cnmpt2nd  23994  tmdgsum  24420  tsmssplit  24477  cnfldnm  25103  expcn  25199  pcorev2  25355  pi1xfrcnv  25384  rrxip  25717  mbfi1flim  26050  itg2uba  26070  itg2cnlem1  26088  itg2cnlem2  26089  itgitg2  26133  itgss3  26141  itgless  26143  ibladdlem  26146  itgaddlem1  26149  iblabslem  26154  itggt0  26170  itgcn  26171  limcdif  26202  limcres  26212  cnplimc  26213  dvcobr  26272  dvexp  26279  dveflem  26305  dvef  26306  dvlip  26319  dvlipcn  26320  lhop  26342  tdeglem2  26385  plyid  26533  coeidp  26588  dgrid  26589  plymulidp  26609  pserdvlem2  26761  abelth  26774  dvrelog  26971  logcn  26981  dvlog  26985  advlog  26988  advlogexp  26989  logtayl  26994  logccv  26997  dvcxp1  27074  dvsqrt  27076  dvcncxp1  27077  dvcnsqrt  27078  resqrtcn  27083  loglesqrt  27095  logblog  27126  dvatan  27269  leibpilem2  27275  leibpi  27276  efrlim  27303  sqrtlim  27306  amgmlem  27323  emcllem5  27333  lgamgulmlem2  27363  lgam1  27397  chtublem  27544  logfacrlim2  27559  bposlem6  27622  chto1lb  27811  vmadivsum  27815  dchrvmasumlema  27833  mulogsumlem  27864  logdivsum  27866  logsqvma2  27876  log2sumbnd  27877  selberglem1  27878  selberglem3  27880  selberg  27881  selberg2lem  27883  selberg2  27884  pntrmax  27897  pntrsumo1  27898  selbergr  27901  selbergs  27907  pnt2  27946  pnt  27947  ostth2  27970  ostth  27972  hilnormi  31771  bra0  32558  partfun2  33318  mplmonprod  34233  zrhre  34698  qqhre  34699  eulerpartgbij  35051  elmrsubrn  36372  faclim  36604  ptrest  38631  poimirlem19  38651  poimirlem20  38652  poimirlem30  38662  ovoliunnfl  38674  voliunnfl  38676  mbfposadd  38679  dvtan  38682  itg2addnclem  38683  ibladdnclem  38688  itgaddnclem1  38690  iblabsnclem  38695  itggt0cn  38702  ftc1anclem4  38708  ftc1anclem5  38709  ftc1anclem6  38710  ftc1anclem7  38711  ftc1anclem8  38712  dvasin  38716  dvacos  38717  areacirclem1  38720  dfadjliftmap2  39483  dfblockliftmap2  39487  aks6d1c1p5  43256  redvmptabs  43505  readvrec2  43506  readvrec  43507  readvcot  43509  arearect  44311  areaquad  44312  cantnfresb  44420  mptrcllem  44707  dfrcl2  44768  dfrcl3  44769  dftrcl3  44814  dfrtrcl3  44827  dfrtrcl4  44832  lhe4.4ex1a  45407  binomcxplemrat  45428  rnsnf  46293  feqresmptf  46337  limsupresre  46800  limsupvaluzmpt  46821  limsup10ex  46877  liminf10ex  46878  dvnprodlem1  47050  itgsin0pilem1  47054  wallispilem4  47172  wallispi2  47177  stirlinglem1  47178  stirlinglem3  47180  dirkercncflem2  47208  fourierdlem48  47258  fourierdlem49  47259  fourierdlem56  47266  fourierdlem57  47267  fourierdlem58  47268  fourierdlem62  47272  fourierdlem107  47317  fouriersw  47335  etransclem46  47384  sge0tsms  47484  sge0less  47496  sge0iun  47523  meadjun  47566  ovn02  47672  hoidmv1le  47698  hspmbllem2  47731  smflimsuplem3  47926  sqrtnpoly  48037  indprm  48808  indprmfz  48809  ackval1  49887  ackval2  49888  ackval3  49889  dftermo4  50731  dvsec  51025  dvcsc  51026  dvcot  51027