Theorem feq2i 6699

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

Syntax hints:   ↔ wb 209   = wceq 1570  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-fn 6541  df-f 6542

This theorem is referenced by:  fresaun  6751  fmpox  8065  fmpo  8066  tposf  8251  issmo  8336  axdc3lem4  10438  cardf  10535  smobeth  10572  seqf2  14059  hashfxnn0  14375  snopiswrd  14562  iswrddm0  14577  s1dm  14648  s2dm  14929  s7f1o  15005  ntrivcvgtail  15956  vdwlem8  17049  0ram  17081  gsumws1  18898  ga0  19369  efgsp1  19808  efgsfo  19810  efgredleme  19814  efgred  19819  ablfaclem2  20159  islinds2  21944  rhmply1vsca  22526  pmatcollpw3fi1lem1  22924  0met  24504  dvef  26120  dvfsumrlim2  26172  dchrisum0  27665  noxp1o  27808  trgcgrg  28765  tgcgr4  28781  axlowdimlem4  29276  uhgr0e  29402  vtxdumgrval  29817  wlkp1  30010  pthdlem2  30098  0wlk  30448  0spth  30458  0clwlkv  30463  wlk2v2e  30489  wlkl0  30699  padct  33044  wrdpmtrlast  33394  mbfmcnt  34639  coinfliprv  34854  rankfo  35486  matunitlindf  38250  fdc  38377  grposnOLD  38514  rabren3dioph  43525  amgm2d  44907  amgm3d  44908  fourierdlem80  46883  sge0iun  47116  0ome  47226  issmflem  47424  2ffzoeq  48048  nnsum4primesodd  48544  nnsum4primesoddALTV  48545  nnsum4primeseven  48548  nnsum4primesevenALTV  48549  line2x  49517  line2y  49518  amgmw2d  50587