Theorem feq12d 6656

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542  ⟶wf 6494

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-fun 6500  df-fn 6501  df-f 6502

This theorem is referenced by:  feq123d  6657  fprg  7109  smoeq  8290  oif  9445  1fv  13601  catcisolem  18077  hofcl  18225  dmdprd  19975  dpjf  20034  pjf2  21694  mat1dimmul  22441  lmbr2  23224  lmff  23266  dfac14  23583  lmmbr2  25226  lmcau  25280  perfdvf  25870  dvnfre  25919  dvle  25974  dvfsumle  25988  dvfsumge  25989  dvmptrecl  25991  uhgr0e  29140  uhgrstrrepe  29147  incistruhgr  29148  upgr1e  29182  1hevtxdg1  29575  umgr2v2e  29594  iswlk  29679  0wlkons1  30191  resf1o  32803  ismeas  34343  omsmeas  34467  breprexplema  34774  satfun  35593  mbfresfi  37987  sdclem1  38064  dfac21  43494  fnlimfvre  46102  climrescn  46176  fourierdlem74  46608  fourierdlem103  46637  fourierdlem104  46638  sge0iunmpt  46846  ismea  46879  isome  46922  sssmf  47166  smflimlem3  47201  smflimlem4  47202  isupwlk  48612  fmpodg  49344  fucof1  49797