Theorem fneq1d 5895

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

Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   Fn wfn 5799

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-br 4584  df-opab 4644  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-fun 5806  df-fn 5807

This theorem is referenced by:  fneq12d  5897  f1o00  6083  f1oprswap  6092  f1ompt  6290  fmpt2d  6300  f1ocnvd  6782  offn  6806  offval2f  6807  offval2  6812  ofrfval2  6813  caofinvl  6822  suppsnop  7196  omxpenlem  7946  itunifn  9122  konigthlem  9269  seqof  12720  swrdlen  13275  mptfzshft  14352  fsumrev  14353  fprodrev  14546  prdsdsfn  15948  imasdsfn  15997  xpscfn  16042  cidfn  16163  comffn  16188  isoval  16248  invf1o  16252  isofn  16258  brssc  16297  cofucl  16371  estrchomfn  16598  funcestrcsetclem4  16606  funcsetcestrclem4  16621  1stfcl  16660  2ndfcl  16661  prfcl  16666  evlfcl  16685  curf1cl  16691  curfcl  16695  hofcl  16722  yonedainv  16744  grpinvf1o  17308  pmtrrn  17700  pmtrfrn  17701  srngf1o  18677  ofco2  20076  mat1dimscm  20100  neif  20714  fmf  21559  fncpn  23502  mdeg0  23634  tglnfn  25242  grpoinvf  26770  kbass2  28360  fnresin  28812  f1o3d  28813  f1od2  28887  pstmxmet  29268  ofcfn  29489  ofcfval2  29493  signstlen  29970  bnj941  30097  msubrn  30680  poimirlem4  32583  cnambfre  32628  sdclem2  32708  diafn  35341  dibfna  35461  dicfnN  35490  dihf11lem  35573  mapd1o  35955  hdmapfnN  36139  hgmapfnN  36198  hbtlem7  36714  fsovf1od  37330  ntrrn  37440  ntrf  37441  dssmapntrcls  37446  addrfn  37697  subrfn  37698  mulvfn  37699  fsumsermpt  38646  hoidmvlelem3  39487  rnghmresfn  41755  rhmresfn  41801  funcringcsetcALTV2lem4  41831  funcringcsetclem4ALTV  41854  rhmsubclem1  41878  rhmsubcALTVlem1  41897