Theorem feq12d 6694

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

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

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 2147  ax-9 2155  ax-ext 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-fun 6539  df-fn 6540  df-f 6541

This theorem is used by:  feq123d  6695  fprg  7156  fmpodg  8073  smoeq  8343  oif  9506  1fv  13706  catcisolem  18205  hofcl  18353  dmdprd  20133  dpjf  20192  pjf2  21933  mat1dimmul  22704  lmbr2  23490  lmff  23532  dfac14  23850  lmmbr2  25493  lmcau  25547  perfdvf  26137  dvnfre  26186  dvle  26241  dvfsumle  26255  dvfsumge  26256  dvmptrecl  26258  uhgr0e  29536  uhgrstrrepe  29543  incistruhgr  29544  upgr1e  29578  1hevtxdg1  29974  umgr2v2e  29993  iswlk  30078  0wlkons1  30599  resf1o  33209  selvply1rhmlemb  34037  ismeas  34718  omsmeas  34842  breprexplema  35146  satfun  35998  mbfresfi  38423  sdclem1  38501  dfac21  43915  fnlimfvre  46510  climrescn  46584  fourierdlem74  47016  fourierdlem103  47045  fourierdlem104  47046  sge0iunmpt  47254  ismea  47287  isome  47330  smflimlem3  47609  smflimlem4  47610  isupwlk  49060  fucof1  50256