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

Theorem feq2i 5722
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 5712 . 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 1379   -->wf 5582
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5589  df-f 5590
This theorem is referenced by:  fresaun  5754  fmpt2x  6847  fmpt2  6848  tposf  6980  issmo  7016  axdc3lem4  8829  cardf  8921  smobeth  8957  1fv  11785  seqf2  12090  hashf  12376  wrd0  12527  iswrddm0  12529  wrd2pr2op  12844  vdwlem8  14361  0ram  14393  gsumws1  15830  ga0  16131  efgsp1  16551  efgsfo  16553  efgredleme  16557  efgred  16562  ablfaclem2  16927  islinds2  18615  pmatcollpw3fi1lem1  19054  0met  20604  dvef  22116  dvfsumrlim2  22168  dchrisum0  23433  trgcgrg  23634  axlowdimlem4  23924  uhgra0  23985  umgra0  24001  0wlk  24223  0trl  24224  wlkntrl  24240  0spth  24249  constr1trl  24266  constr2wlk  24276  constr2trl  24277  usgra2wlkspthlem2  24296  constr3trllem3  24328  constr3trllem4  24329  grposn  24893  mbfmcnt  27879  coinfliprv  28061  ntrivcvgtail  28611  fdc  29841  rabren3dioph  30353  fourierdlem80  31487  2ffzoeq  31810  uhg0e  31845
  Copyright terms: Public domain W3C validator