Theorem fneq1d 6585

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-fun 6494  df-fn 6495

This theorem is referenced by:  fneq12d  6587  f1o00  6809  f1oprswap  6819  f1ompt  7057  fmpt2d  7071  f1ocnvd  7611  offn  7637  offval2f  7639  offval2  7644  ofrfval2  7645  caofinvl  7656  fsplitfpar  8061  omxpenlem  9009  itunifn  10330  konigthlem  10482  seqof  14012  swrdlen  14601  mptfzshft  15731  prdsdsfn  17419  imasdsfn  17469  cidfn  17636  comffn  17662  isoval  17723  invf1o  17727  isofn  17733  brssc  17772  cofucl  17846  estrchomfn  18092  funcestrcsetclem4  18100  funcsetcestrclem4  18115  1stfcl  18154  2ndfcl  18155  prfcl  18160  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  yonedainv  18238  smndex1n0mnd  18874  grpinvf1o  18976  ghmquskerco  19250  pmtrrn  19423  pmtrfrn  19424  rnghmresfn  20587  rhmresfn  20616  rhmsubclem1  20653  srngf1o  20816  ofco2  22426  mat1dimscm  22450  neif  23075  fmf  23920  fncpn  25910  mdeg0  26045  om2noseqfo  28304  noseqrdglem  28311  noseqrdgfn  28312  noseqrdg0  28313  tglnfn  28629  grpoinvf  30618  kbass2  32203  fnresin  32712  f1o3d  32714  suppovss  32769  f1od2  32807  prodindf  32937  esplyfval3  33731  frlmdim  33771  pstmxmet  34057  ofcfn  34260  ofcfval2  34264  signstlen  34727  bnj941  34931  satfn  35553  msubrn  35727  poimirlem4  37959  cnambfre  38003  sdclem2  38077  diafn  41494  dibfna  41614  dicfnN  41643  dihf11lem  41726  mapd1o  42108  hdmapfnN  42289  hgmapfnN  42348  aks4d1p1p5  42528  hbtlem7  43571  fsovf1od  44461  ntrrn  44567  ntrf  44568  dssmapntrcls  44573  addrfn  44916  subrfn  44917  mulvfn  44918  fsumsermpt  46027  hoidmvlelem3  47043  smflimsuplem7  47272  rhmsubcALTVlem1  48769  funcringcsetcALTV2lem4  48781  funcringcsetclem4ALTV  48804  ackvalsucsucval  49176  sectfn  49516  invfn  49517  isofnALT  49518  iinfssclem2  49542  nelsubclem  49554  upeu4  49683  swapf2fn  49755  fucofn2  49811  fucofn22  49827  fucoppc  49897