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

Theorem feq2i 5659
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 5650 . 2  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
31, 2ax-mp 5 1  |-  ( F : A --> C  <->  F : B
--> C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1370   -->wf 5521
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2446  df-fn 5528  df-f 5529
This theorem is referenced by:  fresaun  5689  fmpt2x  6749  fmpt2  6750  tposf  6882  issmo  6918  axdc3lem4  8732  cardf  8824  smobeth  8860  1fv  11648  seqf2  11941  hashf  12226  wrd0  12369  iswrddm0  12371  wrd2pr2op  12664  vdwlem8  14166  0ram  14198  gsumws1  15635  ga0  15934  efgsp1  16354  efgsfo  16356  efgredleme  16360  efgred  16365  ablfaclem2  16708  islinds2  18366  0met  20072  dvef  21584  dvfsumrlim2  21636  dchrisum0  22901  trgcgrg  23102  axlowdimlem4  23342  uhgra0  23394  umgra0  23410  0wlk  23595  0trl  23596  wlkntrl  23612  0spth  23621  constr1trl  23638  constr2wlk  23648  constr2trl  23649  constr3trllem3  23689  constr3trllem4  23690  grposn  23853  mbfmcnt  26826  coinfliprv  27008  ntrivcvgtail  27558  fdc  28788  rabren3dioph  29301  2ffzoeq  30361  usgra2wlkspthlem2  30444  pmatcollpw3fi1lem1  31258
  Copyright terms: Public domain W3C validator