Theorem feq2i 6660

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 6647	. 2 ⊢ (𝐴 = 𝐵 → (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶))
3	1, 2	ax-mp 5	1 ⊢ (𝐹:𝐴⟶𝐶 ↔ 𝐹:𝐵⟶𝐶)

Syntax hints:   ↔ wb 206   = wceq 1542  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-fn 6501  df-f 6502

This theorem is referenced by:  fresaun  6711  fmpox  8020  fmpo  8021  tposf  8204  issmo  8288  axdc3lem4  10375  cardf  10472  smobeth  10509  seqf2  13983  hashfxnn0  14299  snopiswrd  14485  iswrddm0  14500  s1dm  14571  s2dm  14852  s7f1o  14928  ntrivcvgtail  15865  vdwlem8  16959  0ram  16991  gsumws1  18806  ga0  19273  efgsp1  19712  efgsfo  19714  efgredleme  19718  efgred  19723  ablfaclem2  20063  islinds2  21793  rhmply1vsca  22353  pmatcollpw3fi1lem1  22751  0met  24331  dvef  25947  dvfsumrlim2  25999  dchrisum0  27483  noxp1o  27627  trgcgrg  28583  tgcgr4  28599  axlowdimlem4  29014  uhgr0e  29140  vtxdumgrval  29555  wlkp1  29748  pthdlem2  29836  0wlk  30186  0spth  30196  0clwlkv  30201  wlk2v2e  30227  wlkl0  30437  padct  32791  wrdpmtrlast  33154  mbfmcnt  34412  coinfliprv  34627  matunitlindf  37939  fdc  38066  grposnOLD  38203  rabren3dioph  43243  amgm2d  44625  amgm3d  44626  fourierdlem80  46614  sge0iun  46847  0ome  46957  issmflem  47155  2ffzoeq  47776  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  line2x  49230  line2y  49231  amgmw2d  50279