Theorem feq12d 6504

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1537  ⟶wf 6353

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-fun 6359  df-fn 6360  df-f 6361

This theorem is referenced by:  feq123d  6505  fprg  6919  smoeq  7989  oif  8996  1fv  13029  catcisolem  17368  hofcl  17511  dmdprd  19122  dpjf  19181  pjf2  20860  mat1dimmul  21087  lmbr2  21869  lmff  21911  dfac14  22228  lmmbr2  23864  lmcau  23918  perfdvf  24503  dvnfre  24551  dvle  24606  dvfsumle  24620  dvfsumge  24621  dvmptrecl  24623  uhgr0e  26858  uhgrstrrepe  26865  incistruhgr  26866  upgr1e  26900  1hevtxdg1  27290  umgr2v2e  27309  iswlk  27394  0wlkons1  27902  resf1o  30468  ismeas  31460  omsmeas  31583  breprexplema  31903  satfun  32660  mbfresfi  34940  sdclem1  35020  dfac21  39673  fnlimfvre  41962  climrescn  42036  fourierdlem74  42472  fourierdlem103  42501  fourierdlem104  42502  sge0iunmpt  42707  ismea  42740  isome  42783  sssmf  43022  smflimlem3  43056  smflimlem4  43057  isupwlk  44018