Theorem feq2i 6703

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

Syntax hints:   ↔ wb 206   = wceq 1540  ⟶wf 6532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2728  df-fn 6539  df-f 6540

This theorem is referenced by:  fresaun  6754  fmpox  8071  fmpo  8072  tposf  8258  issmo  8367  axdc3lem4  10472  cardf  10569  smobeth  10605  seqf2  14044  hashfxnn0  14360  snopiswrd  14546  iswrddm0  14561  s1dm  14631  s2dm  14914  s7f1o  14990  ntrivcvgtail  15921  vdwlem8  17013  0ram  17045  gsumws1  18821  ga0  19286  efgsp1  19723  efgsfo  19725  efgredleme  19729  efgred  19734  ablfaclem2  20074  islinds2  21778  rhmply1vsca  22331  pmatcollpw3fi1lem1  22729  0met  24310  dvef  25941  dvfsumrlim2  25996  dchrisum0  27488  noxp1o  27632  trgcgrg  28499  tgcgr4  28515  axlowdimlem4  28929  uhgr0e  29055  vtxdumgrval  29471  wlkp1  29666  pthdlem2  29755  0wlk  30102  0spth  30112  0clwlkv  30117  wlk2v2e  30143  wlkl0  30353  padct  32702  wrdpmtrlast  33109  mbfmcnt  34305  coinfliprv  34520  matunitlindf  37647  fdc  37774  grposnOLD  37911  rabren3dioph  42805  amgm2d  44189  amgm3d  44190  fourierdlem80  46182  sge0iun  46415  0ome  46525  issmflem  46723  2ffzoeq  47323  nnsum4primesodd  47777  nnsum4primesoddALTV  47778  nnsum4primeseven  47781  nnsum4primesevenALTV  47782  line2x  48701  line2y  48702  amgmw2d  49635