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

Theorem feq2i 6198
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 6188 . 2 (𝐴 = 𝐵 → (𝐹:𝐴𝐶𝐹:𝐵𝐶))
31, 2ax-mp 5 1 (𝐹:𝐴𝐶𝐹:𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wb 196   = wceq 1632  wf 6045
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753  df-fn 6052  df-f 6053
This theorem is referenced by:  fresaun  6236  fmpt2x  7404  fmpt2  7405  tposf  7549  issmo  7614  axdc3lem4  9467  cardf  9564  smobeth  9600  seqf2  13014  hashfxnn0  13318  hashfOLD  13320  snopiswrd  13500  iswrddm0  13515  s1dm  13579  s2dm  13835  ntrivcvgtail  14831  vdwlem8  15894  0ram  15926  gsumws1  17577  ga0  17931  efgsp1  18350  efgsfo  18352  efgredleme  18356  efgred  18361  ablfaclem2  18685  islinds2  20354  pmatcollpw3fi1lem1  20793  0met  22372  dvef  23942  dvfsumrlim2  23994  dchrisum0  25408  trgcgrg  25609  tgcgr4  25625  axlowdimlem4  26024  uhgr0e  26165  vtxdumgrval  26592  wlkp1  26788  pthdlem2  26874  0wlk  27268  0spth  27278  0clwlkv  27283  wlk2v2e  27309  wlkl0  27528  padct  29806  mbfmcnt  30639  coinfliprv  30853  noxp1o  32122  matunitlindf  33720  fdc  33854  grposnOLD  33994  rabren3dioph  37881  amgm2d  39003  amgm3d  39004  fco3  39920  fourierdlem80  40906  sge0iun  41139  0ome  41249  issmflem  41442  2ffzoeq  41848  nnsum4primesodd  42194  nnsum4primesoddALTV  42195  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  amgmw2d  43063
  Copyright terms: Public domain W3C validator