Theorem feq12d 6244

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1653  ⟶wf 6097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2377  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-rab 3098  df-v 3387  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4116  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375  df-br 4844  df-opab 4906  df-rel 5319  df-cnv 5320  df-co 5321  df-dm 5322  df-rn 5323  df-fun 6103  df-fn 6104  df-f 6105

This theorem is referenced by:  feq123d  6245  fprg  6650  smoeq  7686  oif  8677  1fv  12713  catcisolem  17070  hofcl  17214  dmdprd  18713  dpjf  18772  pjf2  20383  mat1dimmul  20608  lmbr2  21392  lmff  21434  dfac14  21750  lmmbr2  23385  lmcau  23439  perfdvf  24008  dvnfre  24056  dvle  24111  dvfsumle  24125  dvfsumge  24126  dvmptrecl  24128  uhgr0e  26306  uhgrstrrepe  26313  incistruhgr  26314  upgr1e  26348  1hevtxdg1  26756  umgr2v2e  26775  iswlk  26860  0wlkons1  27465  resf1o  30023  ismeas  30778  omsmeas  30901  breprexplema  31228  mbfresfi  33944  sdclem1  34026  dfac21  38421  fnlimfvre  40650  climrescn  40724  fourierdlem74  41140  fourierdlem103  41169  fourierdlem104  41170  sge0iunmpt  41378  ismea  41411  isome  41454  sssmf  41693  smflimlem3  41727  smflimlem4  41728  isupwlk  42516