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 1540  ⟶wf 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-fun 6488  df-fn 6489  df-f 6490

This theorem is referenced by:  feq123d  6645  fprg  7093  smoeq  8280  oif  9441  1fv  13568  catcisolem  18035  hofcl  18183  dmdprd  19897  dpjf  19956  pjf2  21639  mat1dimmul  22379  lmbr2  23162  lmff  23204  dfac14  23521  lmmbr2  25175  lmcau  25229  perfdvf  25820  dvnfre  25872  dvle  25928  dvfsumle  25942  dvfsumleOLD  25943  dvfsumge  25944  dvmptrecl  25946  uhgr0e  29034  uhgrstrrepe  29041  incistruhgr  29042  upgr1e  29076  1hevtxdg1  29470  umgr2v2e  29489  iswlk  29574  0wlkons1  30083  resf1o  32686  ismeas  34165  omsmeas  34290  breprexplema  34597  satfun  35383  mbfresfi  37645  sdclem1  37722  dfac21  43039  fnlimfvre  45656  climrescn  45730  fourierdlem74  46162  fourierdlem103  46191  fourierdlem104  46192  sge0iunmpt  46400  ismea  46433  isome  46476  sssmf  46720  smflimlem3  46755  smflimlem4  46756  isupwlk  48121  fmpodg  48854  fucof1  49308