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

Theorem feq2i 5589
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 5580 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2ax-mp 5 1  |-  ( F : A --> C  <->  F : B
--> C )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1653   -->wf 5453
This theorem is referenced by:  fresaun  5617  fmpt2x  6420  fmpt2  6421  tposf  6510  issmo  6613  axdc3lem4  8338  cardf  8430  smobeth  8466  1fv  11125  seqf2  11347  hashf  11630  wrd0  11737  s1cl  11760  vdwlem8  13361  0ram  13393  gsumws1  14790  ga0  15080  efgsp1  15374  efgsfo  15376  efgredleme  15380  efgred  15385  ablfaclem2  15649  0met  18401  dvef  19869  dvfsumrlim2  19921  dchrisum0  21219  uhgra0  21349  umgra0  21365  0wlk  21550  0trl  21551  wlkntrl  21567  0spth  21576  constr1trl  21593  constr2wlk  21603  constr2trl  21604  constr3trllem3  21644  constr3trllem4  21645  grposn  21808  mbfmcnt  24623  coinfliprv  24745  ntrivcvgtail  25233  axlowdimlem4  25889  fdc  26463  rabren3dioph  26890  islinds2  27274  2ffzoeq  28163  iswrd0i  28201  usgra2wlkspthlem2  28345
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-fn 5460  df-f 5461
  Copyright terms: Public domain W3C validator