Theorem feq12d 6644

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  feq123d  6645  fprg  7094  smoeq  8276  oif  9423  1fv  13549  catcisolem  18019  hofcl  18167  dmdprd  19914  dpjf  19973  pjf2  21653  mat1dimmul  22392  lmbr2  23175  lmff  23217  dfac14  23534  lmmbr2  25187  lmcau  25241  perfdvf  25832  dvnfre  25884  dvle  25940  dvfsumle  25954  dvfsumleOLD  25955  dvfsumge  25956  dvmptrecl  25958  uhgr0e  29051  uhgrstrrepe  29058  incistruhgr  29059  upgr1e  29093  1hevtxdg1  29487  umgr2v2e  29506  iswlk  29591  0wlkons1  30103  resf1o  32717  ismeas  34233  omsmeas  34357  breprexplema  34664  satfun  35476  mbfresfi  37726  sdclem1  37803  dfac21  43183  fnlimfvre  45796  climrescn  45870  fourierdlem74  46302  fourierdlem103  46331  fourierdlem104  46332  sge0iunmpt  46540  ismea  46573  isome  46616  sssmf  46860  smflimlem3  46895  smflimlem4  46896  isupwlk  48260  fmpodg  48993  fucof1  49447