Theorem feq2i 6728

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

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

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 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-fn 6564  df-f 6565

This theorem is referenced by:  fresaun  6779  fmpox  8092  fmpo  8093  tposf  8279  issmo  8388  axdc3lem4  10493  cardf  10590  smobeth  10626  seqf2  14062  hashfxnn0  14376  snopiswrd  14561  iswrddm0  14576  s1dm  14646  s2dm  14929  s7f1o  15005  ntrivcvgtail  15936  vdwlem8  17026  0ram  17058  gsumws1  18851  ga0  19316  efgsp1  19755  efgsfo  19757  efgredleme  19761  efgred  19766  ablfaclem2  20106  islinds2  21833  rhmply1vsca  22392  pmatcollpw3fi1lem1  22792  0met  24376  dvef  26018  dvfsumrlim2  26073  dchrisum0  27564  noxp1o  27708  trgcgrg  28523  tgcgr4  28539  axlowdimlem4  28960  uhgr0e  29088  vtxdumgrval  29504  wlkp1  29699  pthdlem2  29788  0wlk  30135  0spth  30145  0clwlkv  30150  wlk2v2e  30176  wlkl0  30386  padct  32731  wrdpmtrlast  33113  mbfmcnt  34270  coinfliprv  34485  matunitlindf  37625  fdc  37752  grposnOLD  37889  rabren3dioph  42826  amgm2d  44211  amgm3d  44212  fourierdlem80  46201  sge0iun  46434  0ome  46544  issmflem  46742  2ffzoeq  47339  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  line2x  48675  line2y  48676  amgmw2d  49323