Theorem feq12d 6689

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570  ⟶wf 6527

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-fun 6533  df-fn 6534  df-f 6535

This theorem is used by:  feq123d  6690  fprg  7151  fmpodg  8072  smoeq  8342  oif  9508  1fv  13761  catcisolem  18265  hofcl  18413  dmdprd  20194  dpjf  20253  pjf2  22000  mat1dimmul  22771  lmbr2  23557  lmff  23599  dfac14  23917  lmmbr2  25560  lmcau  25614  perfdvf  26203  dvnfre  26252  dvle  26307  dvfsumle  26321  dvfsumge  26322  dvmptrecl  26324  uhgr0e  29631  uhgrstrrepe  29638  incistruhgr  29639  upgr1e  29673  1hevtxdg1  30069  umgr2v2e  30088  iswlk  30173  0wlkons1  30694  resf1o  33304  selvply1rhmlemb  34133  ismeas  34814  omsmeas  34938  breprexplema  35242  satfun  36145  mbfresfi  38552  sdclem1  38645  dfac21  44026  fnlimfvre  46628  climrescn  46702  fourierdlem74  47134  fourierdlem103  47163  fourierdlem104  47164  sge0iunmpt  47372  ismea  47405  isome  47448  smflimlem3  47727  smflimlem4  47728  isupwlk  49178  fucof1  50374