Theorem feq2i 6643

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

Syntax hints:   ↔ wb 206   = wceq 1541  ⟶wf 6477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-fn 6484  df-f 6485

This theorem is referenced by:  fresaun  6694  fmpox  7999  fmpo  8000  tposf  8184  issmo  8268  axdc3lem4  10344  cardf  10441  smobeth  10477  seqf2  13928  hashfxnn0  14244  snopiswrd  14430  iswrddm0  14445  s1dm  14516  s2dm  14797  s7f1o  14873  ntrivcvgtail  15807  vdwlem8  16900  0ram  16932  gsumws1  18746  ga0  19211  efgsp1  19650  efgsfo  19652  efgredleme  19656  efgred  19661  ablfaclem2  20001  islinds2  21751  rhmply1vsca  22304  pmatcollpw3fi1lem1  22702  0met  24282  dvef  25912  dvfsumrlim2  25967  dchrisum0  27459  noxp1o  27603  trgcgrg  28494  tgcgr4  28510  axlowdimlem4  28924  uhgr0e  29050  vtxdumgrval  29466  wlkp1  29659  pthdlem2  29747  0wlk  30094  0spth  30104  0clwlkv  30109  wlk2v2e  30135  wlkl0  30345  padct  32699  wrdpmtrlast  33060  mbfmcnt  34279  coinfliprv  34494  matunitlindf  37664  fdc  37791  grposnOLD  37928  rabren3dioph  42854  amgm2d  44237  amgm3d  44238  fourierdlem80  46230  sge0iun  46463  0ome  46573  issmflem  46771  2ffzoeq  47364  nnsum4primesodd  47833  nnsum4primesoddALTV  47834  nnsum4primeseven  47837  nnsum4primesevenALTV  47838  line2x  48792  line2y  48793  amgmw2d  49842