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

Theorem feq2i 6483
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 6473 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2ax-mp 5 1 (𝐹:𝐴𝐶𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wf 6324
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-fn 6331  df-f 6332
This theorem is referenced by:  fresaun  6527  fmpox  7751  fmpo  7752  tposf  7907  issmo  7972  axdc3lem4  9868  cardf  9965  smobeth  10001  seqf2  13389  hashfxnn0  13697  snopiswrd  13870  iswrddm0  13885  s1dm  13957  s2dm  14247  ntrivcvgtail  15251  vdwlem8  16317  0ram  16349  gsumws1  17997  ga0  18423  efgsp1  18858  efgsfo  18860  efgredleme  18864  efgred  18869  ablfaclem2  19204  islinds2  20505  pmatcollpw3fi1lem1  21394  0met  22976  dvef  24586  dvfsumrlim2  24638  dchrisum0  26107  trgcgrg  26312  tgcgr4  26328  axlowdimlem4  26742  uhgr0e  26867  vtxdumgrval  27279  wlkp1  27474  pthdlem2  27560  0wlk  27904  0spth  27914  0clwlkv  27919  wlk2v2e  27945  wlkl0  28155  padct  30484  mbfmcnt  31634  coinfliprv  31848  noxp1o  33278  matunitlindf  35048  fdc  35176  grposnOLD  35313  rabren3dioph  39743  amgm2d  40891  amgm3d  40892  fco3  41844  fourierdlem80  42815  sge0iun  43045  0ome  43155  issmflem  43348  2ffzoeq  43872  nnsum4primesodd  44301  nnsum4primesoddALTV  44302  nnsum4primeseven  44305  nnsum4primesevenALTV  44306  line2x  45155  line2y  45156  amgmw2d  45319
  Copyright terms: Public domain W3C validator