Theorem feq12d 6678

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

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

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 3919  df-un 3921  df-ss 3933  df-nul 4299  df-if 4491  df-sn 4592  df-pr 4594  df-op 4598  df-br 5110  df-opab 5172  df-rel 5647  df-cnv 5648  df-co 5649  df-dm 5650  df-rn 5651  df-fun 6515  df-fn 6516  df-f 6517

This theorem is referenced by:  feq123d  6679  fprg  7129  smoeq  8321  oif  9489  1fv  13614  catcisolem  18078  hofcl  18226  dmdprd  19936  dpjf  19995  pjf2  21629  mat1dimmul  22369  lmbr2  23152  lmff  23194  dfac14  23511  lmmbr2  25165  lmcau  25219  perfdvf  25810  dvnfre  25862  dvle  25918  dvfsumle  25932  dvfsumleOLD  25933  dvfsumge  25934  dvmptrecl  25936  uhgr0e  29004  uhgrstrrepe  29011  incistruhgr  29012  upgr1e  29046  1hevtxdg1  29440  umgr2v2e  29459  iswlk  29544  0wlkons1  30056  resf1o  32659  ismeas  34195  omsmeas  34320  breprexplema  34627  satfun  35398  mbfresfi  37655  sdclem1  37732  dfac21  43048  fnlimfvre  45665  climrescn  45739  fourierdlem74  46171  fourierdlem103  46200  fourierdlem104  46201  sge0iunmpt  46409  ismea  46442  isome  46485  sssmf  46729  smflimlem3  46764  smflimlem4  46765  isupwlk  48114  fmpodg  48845  fucof1  49293