Theorem feq2i 6683

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

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

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-fn 6517  df-f 6518

This theorem is referenced by:  fresaun  6734  fmpox  8049  fmpo  8050  tposf  8236  issmo  8320  axdc3lem4  10413  cardf  10510  smobeth  10546  seqf2  13993  hashfxnn0  14309  snopiswrd  14495  iswrddm0  14510  s1dm  14580  s2dm  14863  s7f1o  14939  ntrivcvgtail  15873  vdwlem8  16966  0ram  16998  gsumws1  18772  ga0  19237  efgsp1  19674  efgsfo  19676  efgredleme  19680  efgred  19685  ablfaclem2  20025  islinds2  21729  rhmply1vsca  22282  pmatcollpw3fi1lem1  22680  0met  24261  dvef  25891  dvfsumrlim2  25946  dchrisum0  27438  noxp1o  27582  trgcgrg  28449  tgcgr4  28465  axlowdimlem4  28879  uhgr0e  29005  vtxdumgrval  29421  wlkp1  29616  pthdlem2  29705  0wlk  30052  0spth  30062  0clwlkv  30067  wlk2v2e  30093  wlkl0  30303  padct  32650  wrdpmtrlast  33057  mbfmcnt  34266  coinfliprv  34481  matunitlindf  37619  fdc  37746  grposnOLD  37883  rabren3dioph  42810  amgm2d  44194  amgm3d  44195  fourierdlem80  46191  sge0iun  46424  0ome  46534  issmflem  46732  2ffzoeq  47332  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  line2x  48747  line2y  48748  amgmw2d  49797