Theorem feq2i 6677

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

Syntax hints:   ↔ wb 208   = wceq 1559  ⟶wf 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-fn 6518  df-f 6519

This theorem is referenced by:  fresaun  6729  fmpox  8042  fmpo  8043  tposf  8227  issmo  8312  axdc3lem4  10403  cardf  10500  smobeth  10537  seqf2  14027  hashfxnn0  14343  snopiswrd  14529  iswrddm0  14544  s1dm  14615  s2dm  14896  s7f1o  14972  ntrivcvgtail  15920  vdwlem8  17014  0ram  17046  gsumws1  18862  ga0  19328  efgsp1  19767  efgsfo  19769  efgredleme  19773  efgred  19778  ablfaclem2  20118  islinds2  21852  rhmply1vsca  22435  pmatcollpw3fi1lem1  22833  0met  24413  dvef  26029  dvfsumrlim2  26081  dchrisum0  27571  noxp1o  27714  trgcgrg  28671  tgcgr4  28687  axlowdimlem4  29102  uhgr0e  29228  vtxdumgrval  29643  wlkp1  29836  pthdlem2  29924  0wlk  30274  0spth  30284  0clwlkv  30289  wlk2v2e  30315  wlkl0  30525  padct  32880  wrdpmtrlast  33233  mbfmcnt  34525  coinfliprv  34740  matunitlindf  38077  fdc  38204  grposnOLD  38341  rabren3dioph  43352  amgm2d  44734  amgm3d  44735  fourierdlem80  46720  sge0iun  46953  0ome  47063  issmflem  47261  2ffzoeq  47882  nnsum4primesodd  48378  nnsum4primesoddALTV  48379  nnsum4primeseven  48382  nnsum4primesevenALTV  48383  line2x  49336  line2y  49337  amgmw2d  50385