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

Theorem feq2i 6175
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 6165 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2ax-mp 5 1 (𝐹:𝐴𝐶𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1631  wf 6025
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853  df-cleq 2764  df-fn 6032  df-f 6033
This theorem is referenced by:  fresaun  6213  fmpt2x  7386  fmpt2  7387  tposf  7532  issmo  7598  axdc3lem4  9477  cardf  9574  smobeth  9610  seqf2  13023  hashfxnn0  13324  hashfOLD  13326  snopiswrd  13506  iswrddm0  13521  s1dm  13584  s2dm  13840  ntrivcvgtail  14835  vdwlem8  15895  0ram  15927  gsumws1  17580  ga0  17934  efgsp1  18353  efgsfo  18355  efgredleme  18359  efgred  18364  ablfaclem2  18689  islinds2  20365  pmatcollpw3fi1lem1  20807  0met  22387  dvef  23959  dvfsumrlim2  24011  dchrisum0  25426  trgcgrg  25627  tgcgr4  25643  axlowdimlem4  26042  uhgr0e  26183  vtxdumgrval  26613  wlkp1  26809  pthdlem2  26895  0wlk  27292  0spth  27302  0clwlkv  27307  wlk2v2e  27333  wlkl0  27554  padct  29833  mbfmcnt  30666  coinfliprv  30880  noxp1o  32149  matunitlindf  33736  fdc  33869  grposnOLD  34009  rabren3dioph  37902  amgm2d  39024  amgm3d  39025  fco3  39936  fourierdlem80  40917  sge0iun  41150  0ome  41260  issmflem  41453  2ffzoeq  41863  nnsum4primesodd  42209  nnsum4primesoddALTV  42210  nnsum4primeseven  42213  nnsum4primesevenALTV  42214  amgmw2d  43078
  Copyright terms: Public domain W3C validator