Theorem feq2i 6500

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

Syntax hints:   ↔ wb 208   = wceq 1533  ⟶wf 6345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814  df-fn 6352  df-f 6353

This theorem is referenced by:  fresaun  6543  fmpox  7759  fmpo  7760  tposf  7914  issmo  7979  axdc3lem4  9869  cardf  9966  smobeth  10002  seqf2  13383  hashfxnn0  13691  snopiswrd  13864  iswrddm0  13882  s1dm  13956  s2dm  14246  ntrivcvgtail  15250  vdwlem8  16318  0ram  16350  gsumws1  17996  ga0  18422  efgsp1  18857  efgsfo  18859  efgredleme  18863  efgred  18868  ablfaclem2  19202  islinds2  20951  pmatcollpw3fi1lem1  21388  0met  22970  dvef  24571  dvfsumrlim2  24623  dchrisum0  26090  trgcgrg  26295  tgcgr4  26311  axlowdimlem4  26725  uhgr0e  26850  vtxdumgrval  27262  wlkp1  27457  pthdlem2  27543  0wlk  27889  0spth  27899  0clwlkv  27904  wlk2v2e  27930  wlkl0  28140  padct  30449  mbfmcnt  31521  coinfliprv  31735  noxp1o  33165  matunitlindf  34884  fdc  35014  grposnOLD  35154  rabren3dioph  39405  amgm2d  40544  amgm3d  40545  fco3  41484  fourierdlem80  42465  sge0iun  42695  0ome  42805  issmflem  42998  2ffzoeq  43522  nnsum4primesodd  43955  nnsum4primesoddALTV  43956  nnsum4primeseven  43959  nnsum4primesevenALTV  43960  line2x  44735  line2y  44736  amgmw2d  44899