Theorem feq2i 6702

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-fn 6542  df-f 6543

This theorem is used by:  fresaun  6754  fmpox  8079  fmpo  8080  tposf  8275  issmo  8360  axdc3lem4  10535  cardf  10638  smobeth  10675  seqf2  14168  hashfxnn0  14485  snopiswrd  14672  iswrddm0  14687  s1dm  14759  s2dm  15046  s7f1o  15125  ntrivcvgtail  16075  vdwlem8  17172  0ram  17204  gsumws1  19040  ga0  19518  efgsp1  19957  efgsfo  19959  efgredleme  19963  efgred  19968  ablfaclem2  20308  islinds2  22125  rhmply1vsca  22709  matunitlindf  23002  pmatcollpw3fi1lem1  23110  0met  24691  dvef  26306  dvfsumrlim2  26358  dchrisum0  27853  noxp1o  28026  trgcgrg  28984  tgcgr4  29000  axlowdimlem4  29529  uhgr0e  29655  vtxdumgrval  30073  wlkp1  30266  pthdlem2  30360  0wlk  30713  0spth  30723  0clwlkv  30728  wlk2v2e  30764  wlkl0  30974  padct  33358  wrdpmtrlast  33701  mbfmcnt  34947  coinfliprv  35162  rankfo  35788  fdc  38773  grposnOLD  38910  rabren3dioph  43916  amgm2d  45292  amgm3d  45293  fourierdlem80  47290  sge0iun  47523  0ome  47633  issmflem  47831  2ffzoeq  48492  nnsum4primesodd  48988  nnsum4primesoddALTV  48989  nnsum4primeseven  48992  nnsum4primesevenALTV  48993  line2x  49960  line2y  49961  amgmw2d  51158