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

Theorem feq2i 5384
Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.)
Hypothesis
Ref Expression
feq2i.1  |-  A  =  B
Assertion
Ref Expression
feq2i  |-  ( F : A --> C  <->  F : B
--> C )

Proof of Theorem feq2i
StepHypRef Expression
1 feq2i.1 . 2  |-  A  =  B
2 feq2 5376 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2ax-mp 8 1  |-  ( F : A --> C  <->  F : B
--> C )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623   -->wf 5251
This theorem is referenced by:  fresaun  5412  fmpt2x  6190  fmpt2  6191  tposf  6262  issmo  6365  axdc3lem4  8079  cardf  8172  smobeth  8208  seqf2  11065  hashf  11344  wrd0  11418  s1cl  11441  vdwlem8  13035  0ram  13067  gsumws1  14462  ga0  14752  efgsp1  15046  efgsfo  15048  efgredleme  15052  efgred  15057  ablfaclem2  15321  0met  17930  dvef  19327  dvfsumrlim2  19379  dchrisum0  20669  grposn  20882  mbfmcnt  23573  coinfliprv  23683  umgra0  23877  axlowdimlem4  24573  algi  25727  fdc  26455  rabren3dioph  26898  islinds2  27283
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fn 5258  df-f 5259
  Copyright terms: Public domain W3C validator