Theorem feq1d 6237

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 6233	. 2 ⊢ (𝐹 = 𝐺 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐹:𝐴⟶𝐵 ↔ 𝐺:𝐴⟶𝐵))

Syntax hints:   → wi 4   ↔ wb 197   = wceq 1637  ⟶wf 6093

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-opab 4907  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-fun 6099  df-fn 6100  df-f 6101

This theorem is referenced by:  feq12d  6240  fco2  6270  fssres2  6283  fresin  6284  fresaun  6286  fmpt3d  6604  fressnfv  6647  off  7138  caofinvl  7150  curry1f  7501  curry2f  7503  f2ndf  7513  eroprf  8077  pmresg  8116  pw2f1olem  8299  ordtypelem4  8661  fseqenlem1  9126  canthp1lem2  9756  fseq1p1m1  12633  repsf  13740  rlimres  14508  lo1res  14509  rpnnen2lem2  15160  1arithlem3  15842  vdwapf  15889  fsets  16098  mrcf  16470  cofucl  16748  funcres  16756  homaf  16880  funcestrcsetclem3  16983  funcestrcsetclem9  16989  funcsetcestrclem3  16997  1stfcl  17038  2ndfcl  17039  prfcl  17044  evlfcl  17063  curf1cl  17069  yonedalem4c  17118  vrmdf  17596  pmtrf  18072  pmtrfinv  18078  pmtrff1o  18080  pmtrfcnv  18081  psgnunilem5  18111  pj1f  18307  efgtf  18332  vrgpf  18378  gsumzres  18507  gsummptfsadd  18521  gsummptfssub  18546  lspf  19177  psrass1lem  19582  subrgpsr  19624  mvrf  19629  coe1f2  19783  isphld  20205  pjf  20264  uvcff  20337  frlmup1  20344  cpm2mf  20767  lmbr  21273  tsmsres  22157  prdsdsf  22382  imasdsf1olem  22388  blfps  22421  blf  22422  nmf2  22607  tngngp2  22666  cphnmf  23204  rrxmet  23402  ovolctb  23470  uniioombllem2  23563  mbfi1fseqlem3  23697  itg2monolem1  23730  itg2monolem2  23731  itg2monolem3  23732  itg2mono  23733  itg2cnlem1  23741  dvres  23888  dvres3a  23891  dvnff  23899  dvcmulf  23921  dvmptcl  23935  dvmptco  23948  dvlipcn  23970  dvgt0lem1  23978  dvle  23983  itgsubstlem  24024  dgrlem  24198  taylpf  24333  taylthlem1  24340  ulmval  24347  ulmshftlem  24356  ulmshft  24357  ulmdvlem1  24367  psergf  24379  pserdvlem2  24395  logbf  24740  lgsfcl3  25256  midf  25881  lmif  25890  vtxdgf  26594  grpodivf  27720  nvmf  27827  imsdf  27871  ipf  27895  0oo  27971  hoaddcl  28944  homulcl  28945  hosubcl  28959  brafn  29133  kbop  29139  off2  29769  fmptcof2  29783  ofoprabco  29790  fpwrelmap  29834  indf1ofs  30412  sitmf  30738  fibp1  30787  ccatmulgnn0dir  30943  reprsuc  31017  cvmliftlem6  31593  cvmliftlem10  31597  mrsubff  31730  msubff  31748  tailf  32689  curf  33698  uncf  33699  poimirlem24  33744  ftc1anclem3  33797  rrnmet  33937  tendoplcl  36559  tendoicl  36574  pw2f1ocnv  38102  itgpowd  38297  seff  39005  expgrowth  39031  feq1dd  39833  dvnmul  40635  dvnprodlem2  40639  dvnprodlem3  40640  voliooicof  40689  stoweidlem34  40727  stoweidlem42  40735  stoweidlem48  40741  dirkerf  40790  fourierdlem41  40841  fourierdlem51  40850  fourierdlem57  40856  fourierdlem60  40859  fourierdlem61  40860  fourierdlem73  40872  fourierdlem75  40874  fourierdlem103  40902  fourierdlem104  40903  etransclem1  40928  etransclem2  40929  etransclem20  40947  etransclem33  40960  etransclem46  40973  sge0isum  41120  sge0seq  41139  isomenndlem  41223  hoicvr  41241  ovnf  41256  ovnsubaddlem1  41263  hsphoif  41269  hoidmvlelem2  41289  hoidmvlelem3  41290  ovnhoilem1  41294  ovnhoilem2  41295  ovncvr2  41304  hoidifhspf  41311  hspmbllem2  41320  iccvonmbllem  41371  vonioolem1  41373  vonioolem2  41374  vonicclem1  41376  vonicclem2  41377  pfxf  41961  1hegrlfgr  42278  funcringcsetcALTV2lem3  42603  funcringcsetcALTV2lem9  42609  funcringcsetclem3ALTV  42626  funcringcsetclem9ALTV  42632  fdivmptf  42900  refdivmptf  42901