Theorem feq1d 6690

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1567  ⟶wf 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5114  df-opab 5178  df-rel 5671  df-cnv 5672  df-co 5673  df-dm 5674  df-rn 5675  df-fun 6541  df-fn 6542  df-f 6543

This theorem is referenced by:  feq1dd  6691  feq12d  6696  fco2  6735  fssres2  6749  fresin  6750  fresaun  6752  fmpt3d  7114  fressnfv  7160  f2ndf  8117  eroprf  8815  pmresg  8870  pw2f1olem  9071  ordtypelem4  9485  canthp1lem2  10640  fseq1p1m1  13628  repsf  14812  rlimres  15611  lo1res  15612  vdwapf  17034  fsets  17231  mrcf  17667  cofucl  17947  funcres  17955  funcestrcsetclem9  18206  1stfcl  18255  2ndfcl  18256  evlfcl  18280  yonedalem4c  18335  pmtrfinv  19533  pmtrff1o  19535  pmtrfcnv  19536  efgtf  19794  gsumzres  19981  isphld  21775  pjf  21834  frlmup1  21919  psrass1lem  22054  coe1f2  22340  lmbr  23386  tsmsres  24272  prdsdsf  24495  imasdsf1olem  24501  blfps  24534  blf  24535  tngngp2  24780  rrxmet  25538  ovolctb  25620  itg2monolem1  25880  itg2monolem2  25881  itg2monolem3  25882  itg2mono  25883  dvres  26041  dvres3a  26044  dvnff  26053  dvcmulf  26075  dvmptcl  26089  dvmptco  26102  dvlipcn  26124  dvgt0lem1  26132  itgsubstlem  26178  itgpowd  26180  dgrlem  26357  taylthlem1  26504  ulmval  26511  lgsfcl3  27450  midf  29045  grpodivf  30833  nvmf  30940  imsdf  30984  ipf  31008  0oo  31084  hoaddcl  32053  homulcl  32054  hosubcl  32068  fmptcof2  32945  ofoprabco  32952  fpwrelmap  33021  indf1ofs  33129  fedgmullem1  33966  sitmf  34689  fibp1  34738  ccatmulgnn0dir  34879  reprsuc  34949  pfxwlk  35551  cvmliftlem6  35717  cvmliftlem10  35721  mrsubff  35939  msubff  35957  tailf  36811  curf  38174  uncf  38175  poimirlem24  38220  ftc1anclem3  38271  rrnmet  38405  tendoplcl  41482  tendoicl  41497  intlewftc  42755  aks6d1c2  42824  aks6d1c6lem3  42866  pw2f1ocnv  43693  seff  44948  expgrowth  44974  dvnmul  46586  dvnprodlem2  46590  dvnprodlem3  46591  voliooicof  46639  stoweidlem34  46677  stoweidlem42  46685  stoweidlem48  46691  dirkerf  46740  fourierdlem41  46791  fourierdlem51  46800  fourierdlem57  46806  fourierdlem60  46809  fourierdlem61  46810  fourierdlem73  46822  fourierdlem75  46824  fourierdlem103  46852  fourierdlem104  46853  etransclem1  46878  etransclem2  46879  etransclem20  46897  etransclem33  46910  etransclem46  46923  sge0isum  47070  sge0seq  47089  isomenndlem  47173  ovnf  47206  ovnsubaddlem1  47213  hsphoif  47219  hoidmvlelem2  47239  hoidmvlelem3  47240  ovnhoilem1  47244  ovnhoilem2  47245  ovncvr2  47254  hoidifhspf  47261  hspmbllem2  47270  iccvonmbllem  47321  vonioolem1  47323  vonioolem2  47324  vonicclem1  47326  vonicclem2  47327  smfsupdmmbllem  47487  smfinfdmmbllem  47491  fsetsniunop  47712  1hegrlfgr  48823  funcringcsetcALTV2lem3  48983  funcringcsetcALTV2lem9  48989  funcringcsetclem3ALTV  49006  funcringcsetclem9ALTV  49012  fdivmptf  49243  refdivmptf  49244  itcovalendof  49371  ackendofnn0  49386  fucoppcid  50108  functermc  50208