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 1541  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  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  7100  smoeq  8282  oif  9435  1fv  13563  catcisolem  18034  hofcl  18182  dmdprd  19929  dpjf  19988  pjf2  21669  mat1dimmul  22420  lmbr2  23203  lmff  23245  dfac14  23562  lmmbr2  25215  lmcau  25269  perfdvf  25860  dvnfre  25912  dvle  25968  dvfsumle  25982  dvfsumleOLD  25983  dvfsumge  25984  dvmptrecl  25986  uhgr0e  29144  uhgrstrrepe  29151  incistruhgr  29152  upgr1e  29186  1hevtxdg1  29580  umgr2v2e  29599  iswlk  29684  0wlkons1  30196  resf1o  32809  ismeas  34356  omsmeas  34480  breprexplema  34787  satfun  35605  mbfresfi  37863  sdclem1  37940  dfac21  43304  fnlimfvre  45914  climrescn  45988  fourierdlem74  46420  fourierdlem103  46449  fourierdlem104  46450  sge0iunmpt  46658  ismea  46691  isome  46734  sssmf  46978  smflimlem3  47013  smflimlem4  47014  isupwlk  48378  fmpodg  49110  fucof1  49563