Theorem feq2i 6739

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

Syntax hints:   ↔ wb 206   = wceq 1537  ⟶wf 6569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-fn 6576  df-f 6577

This theorem is referenced by:  fco3OLD  6781  fresaun  6792  fmpox  8108  fmpo  8109  tposf  8295  issmo  8404  axdc3lem4  10522  cardf  10619  smobeth  10655  seqf2  14072  hashfxnn0  14386  snopiswrd  14571  iswrddm0  14586  s1dm  14656  s2dm  14939  s7f1o  15015  ntrivcvgtail  15948  vdwlem8  17035  0ram  17067  gsumws1  18873  ga0  19338  efgsp1  19779  efgsfo  19781  efgredleme  19785  efgred  19790  ablfaclem2  20130  islinds2  21856  rhmply1vsca  22413  pmatcollpw3fi1lem1  22813  0met  24397  dvef  26038  dvfsumrlim2  26093  dchrisum0  27582  noxp1o  27726  trgcgrg  28541  tgcgr4  28557  axlowdimlem4  28978  uhgr0e  29106  vtxdumgrval  29522  wlkp1  29717  pthdlem2  29804  0wlk  30148  0spth  30158  0clwlkv  30163  wlk2v2e  30189  wlkl0  30399  padct  32733  wrdpmtrlast  33086  mbfmcnt  34233  coinfliprv  34447  matunitlindf  37578  fdc  37705  grposnOLD  37842  rabren3dioph  42771  amgm2d  44160  amgm3d  44161  fourierdlem80  46107  sge0iun  46340  0ome  46450  issmflem  46648  2ffzoeq  47242  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  line2x  48488  line2y  48489  amgmw2d  48898