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

Theorem feq2i 6257
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 6247 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2ax-mp 5 1 (𝐹:𝐴𝐶𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 197   = wceq 1637  wf 6106
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1860  df-cleq 2810  df-fn 6113  df-f 6114
This theorem is referenced by:  fresaun  6299  fmpt2x  7478  fmpt2  7479  tposf  7624  issmo  7690  axdc3lem4  9569  cardf  9666  smobeth  9702  seqf2  13062  hashfxnn0  13363  hashfOLD  13365  snopiswrd  13544  iswrddm0  13559  s1dm  13622  s2dm  13878  ntrivcvgtail  14872  vdwlem8  15928  0ram  15960  gsumws1  17600  ga0  17951  efgsp1  18370  efgsfo  18372  efgredleme  18376  efgred  18381  ablfaclem2  18706  islinds2  20382  pmatcollpw3fi1lem1  20824  0met  22404  dvef  23979  dvfsumrlim2  24031  dchrisum0  25445  trgcgrg  25646  tgcgr4  25662  axlowdimlem4  26061  uhgr0e  26202  vtxdumgrval  26632  wlkp1  26828  pthdlem2  26914  0wlk  27311  0spth  27321  0clwlkv  27326  wlk2v2e  27352  wlkl0  27569  padct  29846  mbfmcnt  30677  coinfliprv  30891  noxp1o  32158  matunitlindf  33738  fdc  33870  grposnOLD  34010  rabren3dioph  37898  amgm2d  39018  amgm3d  39019  fco3  39924  fourierdlem80  40899  sge0iun  41132  0ome  41242  issmflem  41435  2ffzoeq  41930  nnsum4primesodd  42276  nnsum4primesoddALTV  42277  nnsum4primeseven  42280  nnsum4primesevenALTV  42281  amgmw2d  43138
  Copyright terms: Public domain W3C validator