Theorem feq1d 5943

Description: Equality deduction for functions. (Contributed by NM, 19-Feb-2008.)

Hypothesis

Ref	Expression
feq1d.1	⊢ (𝜑 → 𝐹 = 𝐺)

Assertion

Ref	Expression
feq1d	⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Proof of Theorem feq1d

Step	Hyp	Ref	Expression
1		feq1d.1	. 2 ⊢ (𝜑 → 𝐹 = 𝐺)
2		feq1 5939	. 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475  ⟶wf 5800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-fun 5806  df-fn 5807  df-f 5808

This theorem is referenced by:  feq12d  5946  fco2  5972  fssres2  5985  fresin  5986  fresaun  5988  fmpt3d  6293  fressnfv  6332  off  6810  caofinvl  6822  curry1f  7158  curry2f  7160  f2ndf  7170  eroprf  7732  pmresg  7771  pw2f1olem  7949  ordtypelem4  8309  fseqenlem1  8730  canthp1lem2  9354  fseq1p1m1  12283  repsf  13371  rlimres  14137  lo1res  14138  rpnnen2lem2  14783  1arithlem3  15467  vdwapf  15514  fsets  15723  mrcf  16092  cofucl  16371  funcres  16379  homaf  16503  funcestrcsetclem3  16605  funcestrcsetclem9  16611  funcsetcestrclem3  16619  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlfcl  16685  curf1cl  16691  yonedalem4c  16740  vrmdf  17218  pmtrf  17698  pmtrfinv  17704  pmtrff1o  17706  pmtrfcnv  17707  psgnunilem5  17737  pj1f  17933  efgtf  17958  vrgpf  18004  gsumzres  18133  gsummptfsadd  18147  gsummptfssub  18172  lspf  18795  psrass1lem  19198  subrgpsr  19240  mvrf  19245  coe1f2  19400  isphld  19818  pjf  19876  uvcff  19949  frlmup1  19956  cpm2mf  20376  lmbr  20872  tsmsres  21757  prdsdsf  21982  imasdsf1olem  21988  blfps  22021  blf  22022  nmf2  22207  tngngp2  22266  cphnmf  22803  rrxmet  22999  ovolctb  23065  uniioombllem2  23157  mbfi1fseqlem3  23290  itg2monolem1  23323  itg2monolem2  23324  itg2monolem3  23325  itg2mono  23326  itg2cnlem1  23334  dvres  23481  dvres3a  23484  dvnff  23492  dvcmulf  23514  dvmptcl  23528  dvmptco  23541  dvlipcn  23561  dvgt0lem1  23569  dvle  23574  itgsubstlem  23615  dgrlem  23789  taylpf  23924  taylthlem1  23931  ulmval  23938  ulmshftlem  23947  ulmshft  23948  ulmdvlem1  23958  psergf  23970  pserdvlem2  23986  logbf  24327  lgsfcl3  24843  midf  25468  lmif  25477  vdgrf  26425  vdgrfif  26426  grpodivf  26776  nvmf  26884  imsdf  26928  ipf  26952  0oo  27028  hoaddcl  28001  homulcl  28002  hosubcl  28016  brafn  28190  kbop  28196  off2  28823  fmptcof2  28839  ofoprabco  28847  fpwrelmap  28896  indf1ofs  29415  sitmf  29741  fibp1  29790  ccatmulgnn0dir  29945  cvmliftlem6  30526  cvmliftlem10  30530  mrsubff  30663  msubff  30681  tailf  31540  curf  32557  uncf  32558  poimirlem24  32603  ftc1anclem3  32657  rrnmet  32798  tendoplcl  35087  tendoicl  35102  pw2f1ocnv  36622  itgpowd  36819  seff  37530  expgrowth  37556  feq1dd  38341  dvnmul  38833  dvnprodlem2  38837  dvnprodlem3  38838  voliooicof  38889  stoweidlem34  38927  stoweidlem42  38935  stoweidlem48  38941  dirkerf  38990  fourierdlem41  39041  fourierdlem51  39050  fourierdlem57  39056  fourierdlem60  39059  fourierdlem61  39060  fourierdlem73  39072  fourierdlem75  39074  fourierdlem103  39102  fourierdlem104  39103  etransclem1  39128  etransclem2  39129  etransclem20  39147  etransclem33  39160  etransclem46  39173  sge0isum  39320  sge0seq  39339  isomenndlem  39420  hoicvr  39438  ovnf  39453  ovnsubaddlem1  39460  hsphoif  39466  hoidmvlelem2  39486  hoidmvlelem3  39487  ovnhoilem1  39491  ovnhoilem2  39492  ovncvr2  39501  hoidifhspf  39508  hspmbllem2  39517  iccvonmbllem  39569  vonioolem1  39571  vonioolem2  39572  vonicclem1  39574  vonicclem2  39575  pfxf  40252  vtxdgf  40686  1hegrlfgr  40722  funcringcsetcALTV2lem3  41830  funcringcsetcALTV2lem9  41836  funcringcsetclem3ALTV  41853  funcringcsetclem9ALTV  41859  fdivmptf  42133  refdivmptf  42134