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

Theorem feq2i 6500
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 6490 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2ax-mp 5 1 (𝐹:𝐴𝐶𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 207   = wceq 1528  wf 6345
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 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814  df-fn 6352  df-f 6353
This theorem is referenced by:  fresaun  6543  fmpox  7756  fmpo  7757  tposf  7911  issmo  7976  axdc3lem4  9864  cardf  9961  smobeth  9997  seqf2  13379  hashfxnn0  13687  snopiswrd  13860  iswrddm0  13878  s1dm  13952  s2dm  14242  ntrivcvgtail  15246  vdwlem8  16314  0ram  16346  gsumws1  17992  ga0  18368  efgsp1  18794  efgsfo  18796  efgredleme  18800  efgred  18805  ablfaclem2  19139  islinds2  20887  pmatcollpw3fi1lem1  21324  0met  22905  dvef  24506  dvfsumrlim2  24558  dchrisum0  26024  trgcgrg  26229  tgcgr4  26245  axlowdimlem4  26659  uhgr0e  26784  vtxdumgrval  27196  wlkp1  27391  pthdlem2  27477  0wlk  27823  0spth  27833  0clwlkv  27838  wlk2v2e  27864  wlkl0  28074  padct  30382  mbfmcnt  31426  coinfliprv  31640  noxp1o  33068  matunitlindf  34772  fdc  34903  grposnOLD  35043  rabren3dioph  39292  amgm2d  40432  amgm3d  40433  fco3  41371  fourierdlem80  42352  sge0iun  42582  0ome  42692  issmflem  42885  2ffzoeq  43409  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  line2x  44639  line2y  44640  amgmw2d  44803
  Copyright terms: Public domain W3C validator