Theorem feq12d 6679

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540  ⟶wf 6510

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-fun 6516  df-fn 6517  df-f 6518

This theorem is referenced by:  feq123d  6680  fprg  7130  smoeq  8322  oif  9490  1fv  13615  catcisolem  18079  hofcl  18227  dmdprd  19937  dpjf  19996  pjf2  21630  mat1dimmul  22370  lmbr2  23153  lmff  23195  dfac14  23512  lmmbr2  25166  lmcau  25220  perfdvf  25811  dvnfre  25863  dvle  25919  dvfsumle  25933  dvfsumleOLD  25934  dvfsumge  25935  dvmptrecl  25937  uhgr0e  29005  uhgrstrrepe  29012  incistruhgr  29013  upgr1e  29047  1hevtxdg1  29441  umgr2v2e  29460  iswlk  29545  0wlkons1  30057  resf1o  32660  ismeas  34196  omsmeas  34321  breprexplema  34628  satfun  35405  mbfresfi  37667  sdclem1  37744  dfac21  43062  fnlimfvre  45679  climrescn  45753  fourierdlem74  46185  fourierdlem103  46214  fourierdlem104  46215  sge0iunmpt  46423  ismea  46456  isome  46499  sssmf  46743  smflimlem3  46778  smflimlem4  46779  isupwlk  48128  fmpodg  48861  fucof1  49315