Theorem mpteq2ia 4740

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 2622	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1722	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2ia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
4	3	rgen 2922	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶
5		mpteq12f 4731	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
6	2, 4, 5	mp2an 708	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4  ∀wal 1481   = wceq 1483   ∈ wcel 1990  ∀wral 2912   ↦ cmpt 4729

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ral 2917  df-opab 4713  df-mpt 4730

This theorem is referenced by:  mpteq2i  4741  feqresmpt  6250  elfvmptrab  6306  fmptap  6436  offres  7163  resixpfo  7946  dfoi  8416  cantnflem1d  8585  cantnflem1  8586  dfceil2  12640  dfid5  13767  dfid6  13768  cnrecnv  13905  ackbijnn  14560  harmonic  14591  ege2le3  14820  eirrlem  14932  prmrec  15626  imasdsval2  16176  cayleylem1  17832  pmtrprfval  17907  gsumzsplit  18327  gsum2dlem2  18370  dmdprdsplitlem  18436  coe1sclmul  19652  coe1sclmul2  19654  frlmip  20117  mdetunilem9  20426  leordtvallem1  21014  leordtvallem2  21015  txkgen  21455  cnmpt1st  21471  cnmpt2nd  21472  tmdgsum  21899  tsmssplit  21955  cnfldnm  22582  expcn  22675  pcorev2  22828  pi1xfrcnv  22857  rrxip  23178  mbfi1flim  23490  itg2uba  23510  itg2cnlem1  23528  itg2cnlem2  23529  itgitg2  23573  itgss3  23581  itgless  23583  ibladdlem  23586  itgaddlem1  23589  iblabslem  23594  itggt0  23608  itgcn  23609  limcdif  23640  limcres  23650  cnplimc  23651  dvcobr  23709  dvexp  23716  dveflem  23742  dvef  23743  dvlip  23756  dvlipcn  23757  lhop  23779  tdeglem2  23821  plyid  23965  coeidp  24019  dgrid  24020  pserdvlem2  24182  abelth  24195  dvrelog  24383  logcn  24393  dvlog  24397  advlog  24400  advlogexp  24401  logtayl  24406  logccv  24409  dvcxp1  24481  dvsqrt  24483  dvcncxp1  24484  dvcnsqrt  24485  resqrtcn  24490  loglesqrt  24499  logblog  24530  dvatan  24662  leibpilem2  24668  leibpi  24669  efrlim  24696  sqrtlim  24699  amgmlem  24716  emcllem5  24726  lgamgulmlem2  24756  lgam1  24790  chtublem  24936  logfacrlim2  24951  bposlem6  25014  chto1lb  25167  vmadivsum  25171  dchrvmasumlema  25189  mulogsumlem  25220  logdivsum  25222  logsqvma2  25232  log2sumbnd  25233  selberglem1  25234  selberglem3  25236  selberg  25237  selberg2lem  25239  selberg2  25240  pntrmax  25253  pntrsumo1  25254  selbergr  25257  selbergs  25263  pnt2  25302  pnt  25303  ostth2  25326  ostth  25328  hilnormi  28020  bra0  28809  partfun  29475  zrhre  30063  qqhre  30064  eulerpartgbij  30434  plymulx  30625  faclim  31632  ptrest  33408  poimirlem19  33428  poimirlem20  33429  poimirlem30  33439  ovoliunnfl  33451  voliunnfl  33453  mbfposadd  33457  dvtan  33460  itg2addnclem  33461  ibladdnclem  33466  itgaddnclem1  33468  iblabsnclem  33473  itggt0cn  33482  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  dvasin  33496  dvacos  33497  areacirclem1  33500  arearect  37801  areaquad  37802  mptrcllem  37920  dfrcl2  37966  dfrcl3  37967  dftrcl3  38012  dfrtrcl3  38025  dfrtrcl4  38030  lhe4.4ex1a  38528  binomcxplemrat  38549  rnsnf  39370  feqresmptf  39433  limsupresre  39928  limsupvaluzmpt  39949  limsup10ex  40005  liminf10ex  40006  dvnprodlem1  40161  itgsin0pilem1  40165  wallispilem4  40285  wallispi2  40290  stirlinglem1  40291  stirlinglem3  40293  dirkercncflem2  40321  fourierdlem48  40371  fourierdlem49  40372  fourierdlem56  40379  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  fourierdlem107  40430  fouriersw  40448  etransclem46  40497  sge0tsms  40597  sge0less  40609  sge0iun  40636  meadjun  40679  ovn02  40782  hoidmv1le  40808  hspmbllem2  40841  smflimsuplem3  41028