Theorem feq12d 6265

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

Syntax hints:   → wi 4   ↔ wb 198   = wceq 1658  ⟶wf 6118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rab 3125  df-v 3415  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-br 4873  df-opab 4935  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-fun 6124  df-fn 6125  df-f 6126

This theorem is referenced by:  feq123d  6266  fprg  6672  smoeq  7712  oif  8703  1fv  12752  catcisolem  17107  hofcl  17251  dmdprd  18750  dpjf  18809  pjf2  20420  mat1dimmul  20649  lmbr2  21433  lmff  21475  dfac14  21791  lmmbr2  23426  lmcau  23480  perfdvf  24065  dvnfre  24113  dvle  24168  dvfsumle  24182  dvfsumge  24183  dvmptrecl  24185  uhgr0e  26368  uhgrstrrepe  26375  incistruhgr  26376  upgr1e  26410  1hevtxdg1  26803  umgr2v2e  26822  iswlk  26907  0wlkons1  27496  resf1o  30052  ismeas  30806  omsmeas  30929  breprexplema  31256  mbfresfi  33998  sdclem1  34080  dfac21  38478  fnlimfvre  40700  climrescn  40774  fourierdlem74  41190  fourierdlem103  41219  fourierdlem104  41220  sge0iunmpt  41425  ismea  41458  isome  41501  sssmf  41740  smflimlem3  41774  smflimlem4  41775  isupwlk  42563