Theorem fneq1d 6618

Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

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

Assertion

Ref	Expression
fneq1d	⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Proof of Theorem fneq1d

Step	Hyp	Ref	Expression
1		fneq1d.1	. 2 ⊢ (𝜑 → 𝐹 = 𝐺)
2		fneq1 6616	. 2 ⊢ (𝐹 = 𝐺 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))
3	1, 2	syl 18	1 ⊢ (𝜑 → (𝐹 Fn 𝐴 ↔ 𝐺 Fn 𝐴))

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1563   Fn wfn 6520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-fun 6527  df-fn 6528

This theorem is referenced by:  fneq12d  6620  f1o00  6846  f1oprswap  6856  f1ompt  7096  fmpt2d  7110  f1ocnvd  7651  offn  7677  offval2f  7679  offval2  7684  ofrfval2  7685  caofinvl  7696  fsplitfpar  8101  omxpenlem  9054  itunifn  10389  konigthlem  10541  seqof  14086  swrdlen  14675  mptfzshft  15819  prdsdsfn  17508  imasdsfn  17558  cidfn  17725  comffn  17751  isoval  17812  invf1o  17816  isofn  17822  brssc  17861  cofucl  17935  estrchomfn  18181  funcestrcsetclem4  18189  funcsetcestrclem4  18204  1stfcl  18243  2ndfcl  18244  prfcl  18249  evlfcl  18268  curf1cl  18274  curfcl  18278  hofcl  18305  yonedainv  18327  smndex1n0mnd  18964  grpinvf1o  19066  ghmquskerco  19345  pmtrrn  19518  pmtrfrn  19519  rnghmresfn  20695  rhmresfn  20724  rhmsubclem1  20761  srngf1o  20920  ofco2  22569  mat1dimscm  22593  neif  23218  fmf  24063  fncpn  26053  mdeg0  26188  om2noseqfo  28449  noseqrdglem  28456  noseqrdgfn  28457  noseqrdg0  28458  tglnfn  28774  tgplnfn  29005  grpoinvf  30793  kbass2  32378  fnresin  32881  f1o3d  32883  suppovss  32938  f1od2  32976  prodindf  33095  esplyfval3  33879  frlmdim  33918  pstmxmet  34204  ofcfn  34407  ofcfval2  34411  signstlen  34871  bnj941  35078  satfn  35718  msubrn  35892  poimirlem4  38135  cnambfre  38179  sdclem2  38253  diafn  41670  dibfna  41790  dicfnN  41819  dihf11lem  41902  mapd1o  42284  hdmapfnN  42465  hgmapfnN  42524  aks4d1p1p5  42704  hbtlem7  43714  fsovf1od  44604  ntrrn  44710  ntrf  44711  dssmapntrcls  44716  addrfn  45045  subrfn  45046  mulvfn  45047  fsumsermpt  46153  hoidmvlelem3  47169  smflimsuplem7  47398  rhmsubcALTVlem1  48901  funcringcsetcALTV2lem4  48913  funcringcsetclem4ALTV  48936  ackvalsucsucval  49319  sectfn  49658  invfn  49659  isofnALT  49660  iinfssclem2  49684  nelsubclem  49696  upeu4  49825  swapf2fn  49897  fucofn2  49953  fucofn22  49969  fucoppc  50039