Theorem feq2i 6037

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

Step	Hyp	Ref	Expression
1		feq2i.1	. 2 |- A = B
2		feq2 6027	. 2 |- ( A = B -> ( F : A --> C <-> F : B --> C ) )
3	1, 2	ax-mp 5	1 |- ( F : A --> C <-> F : B --> C )

Syntax hints:   <-> wb 196   = wceq 1483   -->wf 5884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615  df-fn 5891  df-f 5892

This theorem is referenced by:  fresaun  6075  fmpt2x  7236  fmpt2  7237  tposf  7380  issmo  7445  axdc3lem4  9275  cardf  9372  smobeth  9408  seqf2  12820  hashfxnn0  13124  hashfOLD  13126  snopiswrd  13314  iswrddm0  13329  s1dm  13388  s2dm  13635  ntrivcvgtail  14632  vdwlem8  15692  0ram  15724  gsumws1  17376  ga0  17731  efgsp1  18150  efgsfo  18152  efgredleme  18156  efgred  18161  ablfaclem2  18485  islinds2  20152  pmatcollpw3fi1lem1  20591  0met  22171  dvef  23743  dvfsumrlim2  23795  dchrisum0  25209  trgcgrg  25410  tgcgr4  25426  axlowdimlem4  25825  uhgr0e  25966  vtxdumgrval  26382  wlkp1  26578  pthdlem2  26664  0wlk  26977  0spth  26987  wlk2v2e  27017  padct  29497  mbfmcnt  30330  coinfliprv  30544  noxp1o  31816  matunitlindf  33407  fdc  33541  grposnOLD  33681  rabren3dioph  37379  amgm2d  38501  amgm3d  38502  fco3  39421  fourierdlem80  40403  sge0iun  40636  0ome  40743  issmflem  40936  2ffzoeq  41338  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  amgmw2d  42550