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

Theorem feq2i 5739
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 5729 . 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 187    = wceq 1437   -->wf 5597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2414  df-fn 5604  df-f 5605
This theorem is referenced by:  fresaun  5771  fmpt2x  6873  fmpt2  6874  tposf  7012  issmo  7078  axdc3lem4  8890  cardf  8982  smobeth  9018  1fv  11915  seqf2  12238  hashf  12528  iswrddm0  12694  wrd0OLD  12696  wrd2pr2op  13022  ntrivcvgtail  13955  vdwlem8  14937  0ram  14977  gsumws1  16622  ga0  16951  efgsp1  17386  efgsfo  17388  efgredleme  17392  efgred  17397  ablfaclem2  17718  islinds2  19369  pmatcollpw3fi1lem1  19808  0met  21379  dvef  22930  dvfsumrlim2  22982  dchrisum0  24356  trgcgrg  24558  tgcgr4  24574  axlowdimlem4  24973  uhgra0  25034  umgra0  25050  0wlk  25273  0trl  25274  wlkntrl  25290  0spth  25299  constr1trl  25316  constr2wlk  25326  constr2trl  25327  usgra2wlkspthlem2  25346  constr3trllem3  25378  constr3trllem4  25379  grposn  25941  padct  28313  mbfmcnt  29098  coinfliprv  29323  fdc  32038  rabren3dioph  35627  amgm2d  36620  amgm3d  36621  fourierdlem80  37990  sge0iun  38169  0ome  38258  nnsum4primesodd  38761  nnsum4primesoddALTV  38762  nnsum4primeseven  38765  nnsum4primesevenALTV  38766  2ffzoeq  38918  uhgr0e  38993  umgr0  39012  uhg0e  39307
  Copyright terms: Public domain W3C validator