Theorem feq12d 5946

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-fun 5806  df-fn 5807  df-f 5808

This theorem is referenced by:  feq123d  5947  fprg  6327  smoeq  7334  oif  8318  1fv  12327  catcisolem  16579  hofcl  16722  dmdprd  18220  dpjf  18279  pjf2  19877  mat1dimmul  20101  lmbr2  20873  lmff  20915  dfac14  21231  lmmbr2  22865  lmcau  22919  perfdvf  23473  dvnfre  23521  dvle  23574  dvfsumle  23588  dvfsumge  23589  dvmptrecl  23591  uhgr0e  25737  uhgrstrrepe  25745  incistruhgr  25746  upgr1e  25779  uhgrac  25834  isumgra  25844  iswlk  26048  istrl  26067  constr1trl  26118  constr3trllem1  26178  eupap1  26503  resf1o  28893  ismeas  29589  omsmeas  29712  mbfresfi  32626  sdclem1  32709  dfac21  36654  fnlimfvre  38741  fourierdlem74  39073  fourierdlem103  39102  fourierdlem104  39103  sge0iunmpt  39311  ismea  39344  isome  39384  sssmf  39625  smflimlem3  39659  smflimlem4  39660  1hevtxdg1  40721  umgr2v2e  40741  is1wlk  40813  isWlk  40814  0wlkOns1  41289