Theorem feq12d 6698

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-fun 6541  df-fn 6542  df-f 6543

This theorem is used by:  feq123d  6699  fprg  7160  fmpodg  8084  smoeq  8362  oif  9528  1fv  13785  catcisolem  18291  hofcl  18439  dmdprd  20220  dpjf  20279  pjf2  22026  mat1dimmul  22797  lmbr2  23583  lmff  23625  dfac14  23943  lmmbr2  25586  lmcau  25640  perfdvf  26229  dvnfre  26278  dvle  26333  dvfsumle  26347  dvfsumge  26348  dvmptrecl  26350  uhgr0e  29655  uhgrstrrepe  29662  incistruhgr  29663  upgr1e  29697  1hevtxdg1  30093  umgr2v2e  30112  iswlk  30197  0wlkons1  30718  resf1o  33369  selvply1rhmlemb  34198  ismeas  34879  omsmeas  35002  breprexplema  35306  satfun  36263  mbfresfi  38678  sdclem1  38771  dfac21  44162  fnlimfvre  46778  climrescn  46852  fourierdlem74  47284  fourierdlem103  47313  fourierdlem104  47314  sge0iunmpt  47522  ismea  47555  isome  47598  smflimlem3  47877  smflimlem4  47878  isupwlk  49328  fucof1  50538