Theorem feq12d 6725

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 6721	. 2 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐴⟶𝐶))
3		feq12d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
4	3	feq2d 6723	. 2 ⊢ (𝜑 → (𝐺:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶))
5	2, 4	bitrd 279	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐶 ↔ 𝐺:𝐵⟶𝐶))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1537  ⟶wf 6559

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 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-fun 6565  df-fn 6566  df-f 6567

This theorem is referenced by:  feq123d  6726  fprg  7175  smoeq  8389  oif  9568  1fv  13684  catcisolem  18164  hofcl  18316  dmdprd  20033  dpjf  20092  pjf2  21752  mat1dimmul  22498  lmbr2  23283  lmff  23325  dfac14  23642  lmmbr2  25307  lmcau  25361  perfdvf  25953  dvnfre  26005  dvle  26061  dvfsumle  26075  dvfsumleOLD  26076  dvfsumge  26077  dvmptrecl  26079  uhgr0e  29103  uhgrstrrepe  29110  incistruhgr  29111  upgr1e  29145  1hevtxdg1  29539  umgr2v2e  29558  iswlk  29643  0wlkons1  30150  resf1o  32748  ismeas  34180  omsmeas  34305  breprexplema  34624  satfun  35396  mbfresfi  37653  sdclem1  37730  dfac21  43055  fnlimfvre  45630  climrescn  45704  fourierdlem74  46136  fourierdlem103  46165  fourierdlem104  46166  sge0iunmpt  46374  ismea  46407  isome  46450  sssmf  46694  smflimlem3  46729  smflimlem4  46730  isupwlk  47980