Theorem feq12d 6722

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

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

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5172  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-fun 6563  df-fn 6564  df-f 6565

This theorem is used by:  feq123d  6723  fprg  7186  fmpodg  8111  smoeq  8389  oif  9554  1fv  13811  catcisolem  18317  hofcl  18465  dmdprd  20247  dpjf  20306  pjf2  22053  mat1dimmul  22824  lmbr2  23610  lmff  23652  dfac14  23970  lmmbr2  25613  lmcau  25667  perfdvf  26256  dvnfre  26305  dvle  26360  dvfsumle  26374  dvfsumge  26375  dvmptrecl  26377  uhgr0e  29682  uhgrstrrepe  29689  incistruhgr  29690  upgr1e  29724  1hevtxdg1  30120  umgr2v2e  30139  iswlk  30224  0wlkons1  30745  resf1o  33395  isedom  33934  selvply1rhmlemb  34234  ismeas  34915  omsmeas  35038  breprexplema  35342  satfun  36356  mbfresfi  38789  sdclem1  38880  dfac21  44272  fnlimfvre  46899  climrescn  46973  fourierdlem74  47405  fourierdlem103  47434  fourierdlem104  47435  sge0iunmpt  47643  ismea  47676  isome  47719  smflimlem3  47998  smflimlem4  47999  isupwlk  49449  fucof1  50659