Theorem feq12d 6693

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-fun 6538  df-fn 6539  df-f 6540

This theorem is used by:  feq123d  6694  fprg  7152  smoeq  8335  oif  9490  1fv  13682  catcisolem  18173  hofcl  18321  dmdprd  20076  dpjf  20135  pjf2  21875  mat1dimmul  22644  lmbr2  23427  lmff  23469  dfac14  23786  lmmbr2  25429  lmcau  25483  perfdvf  26073  dvnfre  26122  dvle  26177  dvfsumle  26191  dvfsumge  26192  dvmptrecl  26194  uhgr0e  29432  uhgrstrrepe  29439  incistruhgr  29440  upgr1e  29474  1hevtxdg1  29867  umgr2v2e  29886  iswlk  29971  0wlkons1  30483  resf1o  33086  selvply1rhmlemb  33918  ismeas  34598  omsmeas  34722  breprexplema  35026  satfun  35911  mbfresfi  38345  sdclem1  38422  dfac21  43821  fnlimfvre  46416  climrescn  46490  fourierdlem74  46922  fourierdlem103  46951  fourierdlem104  46952  sge0iunmpt  47160  ismea  47193  isome  47236  smflimlem3  47515  smflimlem4  47516  isupwlk  48929  fmpodg  49675  fucof1  50128