Theorem feq12d 6700

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-fun 6545  df-fn 6546  df-f 6547

This theorem is used by:  feq123d  6701  fprg  7159  smoeq  8346  oif  9502  1fv  13694  catcisolem  18192  hofcl  18340  dmdprd  20101  dpjf  20160  pjf2  21901  mat1dimmul  22670  lmbr2  23453  lmff  23495  dfac14  23812  lmmbr2  25455  lmcau  25509  perfdvf  26099  dvnfre  26148  dvle  26203  dvfsumle  26217  dvfsumge  26218  dvmptrecl  26220  uhgr0e  29458  uhgrstrrepe  29465  incistruhgr  29466  upgr1e  29500  1hevtxdg1  29893  umgr2v2e  29912  iswlk  29997  0wlkons1  30509  resf1o  33112  selvply1rhmlemb  33940  ismeas  34621  omsmeas  34745  breprexplema  35049  satfun  35924  mbfresfi  38358  sdclem1  38435  dfac21  43834  fnlimfvre  46429  climrescn  46503  fourierdlem74  46935  fourierdlem103  46964  fourierdlem104  46965  sge0iunmpt  47173  ismea  47206  isome  47249  smflimlem3  47528  smflimlem4  47529  isupwlk  48942  fmpodg  49688  fucof1  50141