Theorem mpteq2ia 5159

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 2823	. . 3 ⊢ 𝐴 = 𝐴
2	1	ax-gen 1796	. 2 ⊢ ∀𝑥 𝐴 = 𝐴
3		mpteq2ia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → 𝐵 = 𝐶)
4	3	rgen 3150	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶
5		mpteq12f 5151	. 2 ⊢ ((∀𝑥 𝐴 = 𝐴 ∧ ∀𝑥 ∈ 𝐴 𝐵 = 𝐶) → (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶))
6	2, 4, 5	mp2an 690	1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐶)

Syntax hints:   → wi 4  ∀wal 1535   = wceq 1537   ∈ wcel 2114  ∀wral 3140   ↦ cmpt 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-ral 3145  df-opab 5131  df-mpt 5149

This theorem is referenced by:  mpteq2i  5160  feqresmpt  6736  elfvmptrab  6798  fmptap  6934  offres  7686  resixpfo  8502  dfoi  8977  cantnflem1d  9153  cantnflem1  9154  dfceil2  13212  dfid5  14388  dfid6  14389  cnrecnv  14526  ackbijnn  15185  harmonic  15216  ege2le3  15445  eirrlem  15559  prmrec  16260  imasdsval2  16791  smndex1iidm  18068  smndex2dlinvh  18084  cayleylem1  18542  pmtrprfval  18617  gsumzsplit  19049  gsum2dlem2  19093  dmdprdsplitlem  19161  coe1sclmul  20452  coe1sclmul2  20454  frlmip  20924  mdetunilem9  21231  leordtvallem1  21820  leordtvallem2  21821  txkgen  22262  cnmpt1st  22278  cnmpt2nd  22279  tmdgsum  22705  tsmssplit  22762  cnfldnm  23389  expcn  23482  pcorev2  23634  pi1xfrcnv  23663  rrxip  23995  mbfi1flim  24326  itg2uba  24346  itg2cnlem1  24364  itg2cnlem2  24365  itgitg2  24409  itgss3  24417  itgless  24419  ibladdlem  24422  itgaddlem1  24425  iblabslem  24430  itggt0  24444  itgcn  24445  limcdif  24476  limcres  24486  cnplimc  24487  dvcobr  24545  dvexp  24552  dveflem  24578  dvef  24579  dvlip  24592  dvlipcn  24593  lhop  24615  tdeglem2  24657  plyid  24801  coeidp  24855  dgrid  24856  pserdvlem2  25018  abelth  25031  dvrelog  25222  logcn  25232  dvlog  25236  advlog  25239  advlogexp  25240  logtayl  25245  logccv  25248  dvcxp1  25323  dvsqrt  25325  dvcncxp1  25326  dvcnsqrt  25327  resqrtcn  25332  loglesqrt  25341  logblog  25372  dvatan  25515  leibpilem2  25521  leibpi  25522  efrlim  25549  sqrtlim  25552  amgmlem  25569  emcllem5  25579  lgamgulmlem2  25609  lgam1  25643  chtublem  25789  logfacrlim2  25804  bposlem6  25867  chto1lb  26056  vmadivsum  26060  dchrvmasumlema  26078  mulogsumlem  26109  logdivsum  26111  logsqvma2  26121  log2sumbnd  26122  selberglem1  26123  selberglem3  26125  selberg  26126  selberg2lem  26128  selberg2  26129  pntrmax  26142  pntrsumo1  26143  selbergr  26146  selbergs  26152  pnt2  26191  pnt  26192  ostth2  26215  ostth  26217  hilnormi  28942  bra0  29729  partfun  30423  zrhre  31262  qqhre  31263  eulerpartgbij  31632  plymulx  31820  elmrsubrn  32769  faclim  32980  ptrest  34893  poimirlem19  34913  poimirlem20  34914  poimirlem30  34924  ovoliunnfl  34936  voliunnfl  34938  mbfposadd  34941  dvtan  34944  itg2addnclem  34945  ibladdnclem  34950  itgaddnclem1  34952  iblabsnclem  34957  itggt0cn  34966  ftc1anclem4  34972  ftc1anclem5  34973  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anclem8  34976  dvasin  34980  dvacos  34981  areacirclem1  34984  arearect  39829  areaquad  39830  mptrcllem  39980  dfrcl2  40026  dfrcl3  40027  dftrcl3  40072  dfrtrcl3  40085  dfrtrcl4  40090  lhe4.4ex1a  40668  binomcxplemrat  40689  rnsnf  41451  feqresmptf  41506  limsupresre  41984  limsupvaluzmpt  42005  limsup10ex  42061  liminf10ex  42062  dvnprodlem1  42238  itgsin0pilem1  42242  wallispilem4  42360  wallispi2  42365  stirlinglem1  42366  stirlinglem3  42368  dirkercncflem2  42396  fourierdlem48  42446  fourierdlem49  42447  fourierdlem56  42454  fourierdlem57  42455  fourierdlem58  42456  fourierdlem62  42460  fourierdlem107  42505  fouriersw  42523  etransclem46  42572  sge0tsms  42669  sge0less  42681  sge0iun  42708  meadjun  42751  ovn02  42857  hoidmv1le  42883  hspmbllem2  42916  smflimsuplem3  43103