Theorem feq12d 6699

Description: Equality deduction for functions. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypotheses

Ref	Expression
feq12d.1	⊢ (𝜑 → 𝐹 = 𝐺)
feq12d.2	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
feq12d	⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶))

Proof of Theorem feq12d

Step	Hyp	Ref	Expression
1		feq12d.1	. . 3 ⊢ (𝜑 → 𝐹 = 𝐺)
2	1	feq1d 6695	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐴⟶𝐶))
3		feq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	feq2d 6697	. 2 ⊢ (𝜑 → (𝐺:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶))
5	2, 4	bitrd 279	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6532

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 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125  df-opab 5187  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6538  df-fn 6539  df-f 6540

This theorem is referenced by:  feq123d  6700  fprg  7150  smoeq  8369  oif  9549  1fv  13669  catcisolem  18128  hofcl  18276  dmdprd  19986  dpjf  20045  pjf2  21679  mat1dimmul  22419  lmbr2  23202  lmff  23244  dfac14  23561  lmmbr2  25216  lmcau  25270  perfdvf  25861  dvnfre  25913  dvle  25969  dvfsumle  25983  dvfsumleOLD  25984  dvfsumge  25985  dvmptrecl  25987  uhgr0e  29055  uhgrstrrepe  29062  incistruhgr  29063  upgr1e  29097  1hevtxdg1  29491  umgr2v2e  29510  iswlk  29595  0wlkons1  30107  resf1o  32712  ismeas  34235  omsmeas  34360  breprexplema  34667  satfun  35438  mbfresfi  37695  sdclem1  37772  dfac21  43065  fnlimfvre  45683  climrescn  45757  fourierdlem74  46189  fourierdlem103  46218  fourierdlem104  46219  sge0iunmpt  46427  ismea  46460  isome  46503  sssmf  46747  smflimlem3  46782  smflimlem4  46783  isupwlk  48091  fmpodg  48824  fucof1  49213