Theorem feq12d 6695

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-fun 6540  df-fn 6541  df-f 6542

This theorem is referenced by:  feq123d  6696  fprg  7154  smoeq  8338  oif  9493  1fv  13677  catcisolem  18168  hofcl  18316  dmdprd  20071  dpjf  20130  pjf2  21845  mat1dimmul  22614  lmbr2  23397  lmff  23439  dfac14  23756  lmmbr2  25399  lmcau  25453  perfdvf  26043  dvnfre  26092  dvle  26147  dvfsumle  26161  dvfsumge  26162  dvmptrecl  26164  uhgr0e  29402  uhgrstrrepe  29409  incistruhgr  29410  upgr1e  29444  1hevtxdg1  29837  umgr2v2e  29856  iswlk  29941  0wlkons1  30453  resf1o  33056  selvply1rhmlemb  33890  ismeas  34570  omsmeas  34694  breprexplema  34998  satfun  35884  mbfresfi  38298  sdclem1  38375  dfac21  43776  fnlimfvre  46371  climrescn  46445  fourierdlem74  46877  fourierdlem103  46906  fourierdlem104  46907  sge0iunmpt  47115  ismea  47148  isome  47191  smflimlem3  47470  smflimlem4  47471  isupwlk  48884  fmpodg  49630  fucof1  50083