Theorem feq12d 6650

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-fun 6494  df-fn 6495  df-f 6496

This theorem is referenced by:  feq123d  6651  fprg  7105  smoeq  8287  oif  9442  1fv  13599  catcisolem  18075  hofcl  18223  dmdprd  19973  dpjf  20032  pjf2  21696  mat1dimmul  22466  lmbr2  23249  lmff  23291  dfac14  23608  lmmbr2  25251  lmcau  25305  perfdvf  25895  dvnfre  25944  dvle  25999  dvfsumle  26013  dvfsumge  26014  dvmptrecl  26016  uhgr0e  29165  uhgrstrrepe  29172  incistruhgr  29173  upgr1e  29207  1hevtxdg1  29600  umgr2v2e  29619  iswlk  29704  0wlkons1  30216  resf1o  32829  selvply1rhmlemb  33710  ismeas  34390  omsmeas  34514  breprexplema  34821  satfun  35646  mbfresfi  38040  sdclem1  38117  dfac21  43518  fnlimfvre  46124  climrescn  46198  fourierdlem74  46630  fourierdlem103  46659  fourierdlem104  46660  sge0iunmpt  46868  ismea  46901  isome  46944  sssmf  47188  smflimlem3  47223  smflimlem4  47224  isupwlk  48634  fmpodg  49366  fucof1  49819