Theorem mpteq2ia 5116

Description: An equality inference for the maps-to notation. (Contributed by Mario Carneiro, 16-Dec-2013.)

Hypothesis

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

Assertion

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

Proof of Theorem mpteq2ia

Step	Hyp	Ref	Expression
1		eqid 2759	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1798	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2ia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
4	3	rgen 3078	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶
5		mpteq12f 5108	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
6	2, 4, 5	mp2an 692	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4  ∀wal 1537   = wceq 1539   ∈ wcel 2112  ∀wral 3068   ↦ cmpt 5105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-12 2176  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-tru 1542  df-ex 1783  df-nf 1787  df-sb 2071  df-clab 2737  df-cleq 2751  df-clel 2831  df-ral 3073  df-opab 5088  df-mpt 5106

This theorem is referenced by:  mpteq2i  5117  partfun  6471  feqresmpt  6715  elfvmptrab  6780  fmptap  6916  offres  7681  resixpfo  8511  dfoi  8993  cantnflem1d  9169  cantnflem1  9170  dfceil2  13243  dfid5  14419  dfid6  14420  cnrecnv  14557  ackbijnn  15216  harmonic  15247  ege2le3  15476  eirrlem  15590  prmrec  16298  imasdsval2  16832  dfinito2  17314  dftermo2  17315  dfinito3  17316  dftermo3  17317  smndex1iidm  18117  smndex2dlinvh  18133  cayleylem1  18592  pmtrprfval  18667  gsumzsplit  19100  gsum2dlem2  19144  dmdprdsplitlem  19212  frlmip  20528  coe1sclmul  20991  coe1sclmul2  20993  mdetunilem9  21305  leordtvallem1  21895  leordtvallem2  21896  txkgen  22337  cnmpt1st  22353  cnmpt2nd  22354  tmdgsum  22780  tsmssplit  22837  cnfldnm  23465  expcn  23558  pcorev2  23714  pi1xfrcnv  23743  rrxip  24075  mbfi1flim  24408  itg2uba  24428  itg2cnlem1  24446  itg2cnlem2  24447  itgitg2  24491  itgss3  24499  itgless  24501  ibladdlem  24504  itgaddlem1  24507  iblabslem  24512  itggt0  24528  itgcn  24529  limcdif  24560  limcres  24570  cnplimc  24571  dvcobr  24630  dvexp  24637  dveflem  24663  dvef  24664  dvlip  24677  dvlipcn  24678  lhop  24700  tdeglem2  24746  plyid  24890  coeidp  24944  dgrid  24945  pserdvlem2  25107  abelth  25120  dvrelog  25312  logcn  25322  dvlog  25326  advlog  25329  advlogexp  25330  logtayl  25335  logccv  25338  dvcxp1  25413  dvsqrt  25415  dvcncxp1  25416  dvcnsqrt  25417  resqrtcn  25422  loglesqrt  25431  logblog  25462  dvatan  25605  leibpilem2  25611  leibpi  25612  efrlim  25639  sqrtlim  25642  amgmlem  25659  emcllem5  25669  lgamgulmlem2  25699  lgam1  25733  chtublem  25879  logfacrlim2  25894  bposlem6  25957  chto1lb  26146  vmadivsum  26150  dchrvmasumlema  26168  mulogsumlem  26199  logdivsum  26201  logsqvma2  26211  log2sumbnd  26212  selberglem1  26213  selberglem3  26215  selberg  26216  selberg2lem  26218  selberg2  26219  pntrmax  26232  pntrsumo1  26233  selbergr  26236  selbergs  26242  pnt2  26281  pnt  26282  ostth2  26305  ostth  26307  hilnormi  29030  bra0  29817  zrhre  31473  qqhre  31474  eulerpartgbij  31843  plymulx  32031  elmrsubrn  32983  faclim  33212  ptrest  35321  poimirlem19  35341  poimirlem20  35342  poimirlem30  35352  ovoliunnfl  35364  voliunnfl  35366  mbfposadd  35369  dvtan  35372  itg2addnclem  35373  ibladdnclem  35378  itgaddnclem1  35380  iblabsnclem  35385  itggt0cn  35392  ftc1anclem4  35398  ftc1anclem5  35399  ftc1anclem6  35400  ftc1anclem7  35401  ftc1anclem8  35402  dvasin  35406  dvacos  35407  areacirclem1  35410  arearect  40523  areaquad  40524  mptrcllem  40671  dfrcl2  40733  dfrcl3  40734  dftrcl3  40779  dfrtrcl3  40792  dfrtrcl4  40797  lhe4.4ex1a  41391  binomcxplemrat  41412  rnsnf  42165  feqresmptf  42218  limsupresre  42689  limsupvaluzmpt  42710  limsup10ex  42766  liminf10ex  42767  dvnprodlem1  42939  itgsin0pilem1  42943  wallispilem4  43061  wallispi2  43066  stirlinglem1  43067  stirlinglem3  43069  dirkercncflem2  43097  fourierdlem48  43147  fourierdlem49  43148  fourierdlem56  43155  fourierdlem57  43156  fourierdlem58  43157  fourierdlem62  43161  fourierdlem107  43206  fouriersw  43224  etransclem46  43273  sge0tsms  43370  sge0less  43382  sge0iun  43409  meadjun  43452  ovn02  43558  hoidmv1le  43584  hspmbllem2  43617  smflimsuplem3  43804  ackval1  45445  ackval2  45446  ackval3  45447