Theorem feq2i 6719

Description: Equality inference for functions. (Contributed by NM, 5-Sep-2011.)

Hypothesis

Ref	Expression
feq2i.1	⊢ 𝐴 = 𝐵

Assertion

Ref	Expression
feq2i	⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)

Proof of Theorem feq2i

Step	Hyp	Ref	Expression
1		feq2i.1	. 2 ⊢ 𝐴 = 𝐵
2		feq2 6709	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)

Syntax hints:   ↔ wb 205   = wceq 1533  ⟶wf 6549

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2720  df-fn 6556  df-f 6557

This theorem is referenced by:  fco3OLD  6762  fresaun  6773  fmpox  8077  fmpo  8078  tposf  8266  issmo  8375  axdc3lem4  10484  cardf  10581  smobeth  10617  seqf2  14026  hashfxnn0  14336  snopiswrd  14513  iswrddm0  14528  s1dm  14598  s2dm  14881  ntrivcvgtail  15886  vdwlem8  16964  0ram  16996  gsumws1  18797  ga0  19256  efgsp1  19699  efgsfo  19701  efgredleme  19705  efgred  19710  ablfaclem2  20050  islinds2  21754  pmatcollpw3fi1lem1  22708  0met  24292  dvef  25932  dvfsumrlim2  25987  dchrisum0  27473  noxp1o  27616  trgcgrg  28339  tgcgr4  28355  axlowdimlem4  28776  uhgr0e  28904  vtxdumgrval  29320  wlkp1  29515  pthdlem2  29602  0wlk  29946  0spth  29956  0clwlkv  29961  wlk2v2e  29987  wlkl0  30197  padct  32522  mbfmcnt  33921  coinfliprv  34135  matunitlindf  37124  fdc  37251  grposnOLD  37388  rabren3dioph  42266  amgm2d  43659  amgm3d  43660  fourierdlem80  45603  sge0iun  45836  0ome  45946  issmflem  46144  2ffzoeq  46737  nnsum4primesodd  47165  nnsum4primesoddALTV  47166  nnsum4primeseven  47169  nnsum4primesevenALTV  47170  line2x  47905  line2y  47906  amgmw2d  48315