Theorem feq12d 6650

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  feq123d  6651  fprg  7102  smoeq  8283  oif  9438  1fv  13592  catcisolem  18068  hofcl  18216  dmdprd  19966  dpjf  20025  pjf2  21704  mat1dimmul  22451  lmbr2  23234  lmff  23276  dfac14  23593  lmmbr2  25236  lmcau  25290  perfdvf  25880  dvnfre  25929  dvle  25984  dvfsumle  25998  dvfsumge  25999  dvmptrecl  26001  uhgr0e  29154  uhgrstrrepe  29161  incistruhgr  29162  upgr1e  29196  1hevtxdg1  29590  umgr2v2e  29609  iswlk  29694  0wlkons1  30206  resf1o  32818  ismeas  34359  omsmeas  34483  breprexplema  34790  satfun  35609  mbfresfi  38001  sdclem1  38078  dfac21  43512  fnlimfvre  46120  climrescn  46194  fourierdlem74  46626  fourierdlem103  46655  fourierdlem104  46656  sge0iunmpt  46864  ismea  46897  isome  46940  sssmf  47184  smflimlem3  47219  smflimlem4  47220  isupwlk  48624  fmpodg  49356  fucof1  49809