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

Theorem feq2i 5935
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 5925 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2ax-mp 5 1 (𝐹:𝐴𝐶𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 194   = wceq 1474  wf 5785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602  df-fn 5792  df-f 5793
This theorem is referenced by:  fresaun  5972  fmpt2x  7102  fmpt2  7103  tposf  7244  issmo  7309  axdc3lem4  9135  cardf  9228  smobeth  9264  seqf2  12639  hashf  12943  snopiswrd  13117  iswrddm0  13132  s1dm  13189  s2dm  13433  ntrivcvgtail  14419  vdwlem8  15478  0ram  15510  gsumws1  17147  ga0  17502  efgsp1  17921  efgsfo  17923  efgredleme  17927  efgred  17932  ablfaclem2  18256  islinds2  19918  pmatcollpw3fi1lem1  20357  0met  21928  dvef  23491  dvfsumrlim2  23543  dchrisum0  24953  trgcgrg  25155  tgcgr4  25171  axlowdimlem4  25570  uhgra0  25631  umgra0  25647  0wlk  25868  0trl  25869  wlkntrl  25885  0spth  25894  constr1trl  25911  constr2wlk  25921  constr2trl  25922  usgra2wlkspthlem2  25941  constr3trllem3  25973  constr3trllem4  25974  padct  28678  mbfmcnt  29450  coinfliprv  29664  matunitlindf  32360  fdc  32494  grposnOLD  32634  rabren3dioph  36180  amgm2d  37306  amgm3d  37307  fco3  38199  fourierdlem80  38862  sge0iun  39095  0ome  39202  issmflem  39396  nnsum4primesodd  39996  nnsum4primesoddALTV  39997  nnsum4primeseven  40000  nnsum4primesevenALTV  40001  2ffzoeq  40167  uhgr0e  40277  vtxdumgrval  40682  1wlkp1  40871  pthdlem2  40955  01wlk  41265  0spth-av  41275  1wlk2v2e  41305  amgmw2d  42301
  Copyright terms: Public domain W3C validator