Theorem feq12d 6675

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559  ⟶wf 6513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-rn 5656  df-fun 6519  df-fn 6520  df-f 6521

This theorem is referenced by:  feq123d  6676  fprg  7134  smoeq  8316  oif  9475  1fv  13649  catcisolem  18126  hofcl  18274  dmdprd  20023  dpjf  20082  pjf2  21746  mat1dimmul  22516  lmbr2  23299  lmff  23341  dfac14  23658  lmmbr2  25301  lmcau  25355  perfdvf  25945  dvnfre  25994  dvle  26049  dvfsumle  26063  dvfsumge  26064  dvmptrecl  26066  uhgr0e  29218  uhgrstrrepe  29225  incistruhgr  29226  upgr1e  29260  1hevtxdg1  29653  umgr2v2e  29672  iswlk  29757  0wlkons1  30269  resf1o  32882  selvply1rhmlemb  33777  ismeas  34457  omsmeas  34581  breprexplema  34888  satfun  35725  mbfresfi  38129  sdclem1  38206  dfac21  43607  fnlimfvre  46212  climrescn  46286  fourierdlem74  46718  fourierdlem103  46747  fourierdlem104  46748  sge0iunmpt  46956  ismea  46989  isome  47032  smflimlem3  47311  smflimlem4  47312  isupwlk  48722  fmpodg  49454  fucof1  49907