MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feq2i Structured version   Visualization version   GIF version

Theorem feq2i 6499
Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.)
Hypothesis
Ref Expression
feq2i.1 𝐴 = 𝐵
Assertion
Ref Expression
feq2i (𝐹:𝐴𝐶𝐹:𝐵𝐶)

Proof of Theorem feq2i
StepHypRef Expression
1 feq2i.1 . 2 𝐴 = 𝐵
2 feq2 6489 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2ax-mp 5 1 (𝐹:𝐴𝐶𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528  wf 6344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-fn 6351  df-f 6352
This theorem is referenced by:  fresaun  6542  fmpox  7754  fmpo  7755  tposf  7909  issmo  7974  axdc3lem4  9863  cardf  9960  smobeth  9996  seqf2  13377  hashfxnn0  13685  snopiswrd  13858  iswrddm0  13876  s1dm  13950  s2dm  14240  ntrivcvgtail  15244  vdwlem8  16312  0ram  16344  gsumws1  17990  ga0  18366  efgsp1  18792  efgsfo  18794  efgredleme  18798  efgred  18803  ablfaclem2  19137  islinds2  20885  pmatcollpw3fi1lem1  21322  0met  22903  dvef  24504  dvfsumrlim2  24556  dchrisum0  26023  trgcgrg  26228  tgcgr4  26244  axlowdimlem4  26658  uhgr0e  26783  vtxdumgrval  27195  wlkp1  27390  pthdlem2  27476  0wlk  27822  0spth  27832  0clwlkv  27837  wlk2v2e  27863  wlkl0  28073  padct  30381  mbfmcnt  31425  coinfliprv  31639  noxp1o  33067  matunitlindf  34771  fdc  34901  grposnOLD  35041  rabren3dioph  39290  amgm2d  40429  amgm3d  40430  fco3  41367  fourierdlem80  42348  sge0iun  42578  0ome  42688  issmflem  42881  2ffzoeq  43405  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  line2x  44669  line2y  44670  amgmw2d  44833
  Copyright terms: Public domain W3C validator