Theorem fneq1d 6416

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1538   Fn wfn 6319

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-fun 6326  df-fn 6327

This theorem is referenced by:  fneq12d  6418  f1o00  6624  f1oprswap  6633  f1ompt  6852  fmpt2d  6864  f1ocnvd  7376  offn  7400  offval2f  7401  offval2  7406  ofrfval2  7407  caofinvl  7416  fsplitfpar  7797  omxpenlem  8601  itunifn  9828  konigthlem  9979  seqof  13423  swrdlen  14000  mptfzshft  15125  fprodrev  15323  prdsdsfn  16730  imasdsfn  16779  cidfn  16942  comffn  16967  isoval  17027  invf1o  17031  isofn  17037  brssc  17076  cofucl  17150  estrchomfn  17377  funcestrcsetclem4  17385  funcsetcestrclem4  17400  1stfcl  17439  2ndfcl  17440  prfcl  17445  evlfcl  17464  curf1cl  17470  curfcl  17474  hofcl  17501  yonedainv  17523  smndex1n0mnd  18069  grpinvf1o  18161  pmtrrn  18577  pmtrfrn  18578  srngf1o  19618  ofco2  21056  mat1dimscm  21080  neif  21705  fmf  22550  fncpn  24536  mdeg0  24671  tglnfn  26341  grpoinvf  28315  kbass2  29900  fnresin  30385  f1o3d  30386  suppovss  30443  f1od2  30483  frlmdim  31097  pstmxmet  31250  prodindf  31392  ofcfn  31469  ofcfval2  31473  signstlen  31947  bnj941  32154  satfn  32715  msubrn  32889  poimirlem4  35061  cnambfre  35105  sdclem2  35180  diafn  38330  dibfna  38450  dicfnN  38479  dihf11lem  38562  mapd1o  38944  hdmapfnN  39125  hgmapfnN  39184  hbtlem7  40069  fsovf1od  40717  ntrrn  40825  ntrf  40826  dssmapntrcls  40831  addrfn  41176  subrfn  41177  mulvfn  41178  fsumsermpt  42221  hoidmvlelem3  43236  smflimsuplem7  43457  rnghmresfn  44587  rhmresfn  44633  funcringcsetcALTV2lem4  44663  funcringcsetclem4ALTV  44686  rhmsubclem1  44710  rhmsubcALTVlem1  44728  ackvalsucsucval  45102