Theorem feq2i 6374

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

Syntax hints:   ↔ wb 207   = wceq 1522  ⟶wf 6221

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-9 2091  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1762  df-cleq 2788  df-fn 6228  df-f 6229

This theorem is referenced by:  fresaun  6417  fmpox  7621  fmpo  7622  tposf  7771  issmo  7837  axdc3lem4  9721  cardf  9818  smobeth  9854  seqf2  13239  hashfxnn0  13547  snopiswrd  13716  iswrddm0  13734  s1dm  13806  s2dm  14088  ntrivcvgtail  15089  vdwlem8  16153  0ram  16185  gsumws1  17815  ga0  18169  efgsp1  18590  efgsfo  18592  efgredleme  18596  efgred  18601  ablfaclem2  18925  islinds2  20639  pmatcollpw3fi1lem1  21078  0met  22659  dvef  24260  dvfsumrlim2  24312  dchrisum0  25778  trgcgrg  25983  tgcgr4  25999  axlowdimlem4  26414  uhgr0e  26539  vtxdumgrval  26951  wlkp1  27148  pthdlem2  27236  0wlk  27582  0spth  27592  0clwlkv  27597  wlk2v2e  27623  wlkl0  27838  padct  30143  mbfmcnt  31143  coinfliprv  31357  noxp1o  32779  matunitlindf  34421  fdc  34552  grposnOLD  34692  rabren3dioph  38897  amgm2d  40037  amgm3d  40038  fco3  41031  fourierdlem80  42013  sge0iun  42243  0ome  42353  issmflem  42546  2ffzoeq  43044  nnsum4primesodd  43443  nnsum4primesoddALTV  43444  nnsum4primeseven  43447  nnsum4primesevenALTV  43448  line2x  44222  line2y  44223  amgmw2d  44385