Theorem fneq1d 6600

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1541   Fn wfn 6496

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-fun 6503  df-fn 6504

This theorem is referenced by:  fneq12d  6602  f1o00  6824  f1oprswap  6833  f1ompt  7064  fmpt2d  7076  f1ocnvd  7609  offn  7635  offval2f  7637  offval2  7642  ofrfval2  7643  caofinvl  7652  fsplitfpar  8055  omxpenlem  9024  itunifn  10362  konigthlem  10513  seqof  13975  swrdlen  14547  mptfzshft  15674  prdsdsfn  17361  imasdsfn  17410  cidfn  17573  comffn  17599  isoval  17662  invf1o  17666  isofn  17672  brssc  17711  cofucl  17788  estrchomfn  18036  funcestrcsetclem4  18045  funcsetcestrclem4  18060  1stfcl  18099  2ndfcl  18100  prfcl  18105  evlfcl  18125  curf1cl  18131  curfcl  18135  hofcl  18162  yonedainv  18184  smndex1n0mnd  18736  grpinvf1o  18831  pmtrrn  19253  pmtrfrn  19254  srngf1o  20369  ofco2  21837  mat1dimscm  21861  neif  22488  fmf  23333  fncpn  25334  mdeg0  25472  tglnfn  27552  grpoinvf  29537  kbass2  31122  fnresin  31607  f1o3d  31608  suppovss  31665  f1od2  31706  ghmquskerco  32270  frlmdim  32393  pstmxmet  32567  prodindf  32711  ofcfn  32788  ofcfval2  32792  signstlen  33268  bnj941  33473  satfn  34036  msubrn  34210  poimirlem4  36155  cnambfre  36199  sdclem2  36274  diafn  39570  dibfna  39690  dicfnN  39719  dihf11lem  39802  mapd1o  40184  hdmapfnN  40365  hgmapfnN  40424  aks4d1p1p5  40605  hbtlem7  41510  fsovf1od  42410  ntrrn  42516  ntrf  42517  dssmapntrcls  42522  addrfn  42874  subrfn  42875  mulvfn  42876  fsumsermpt  43940  hoidmvlelem3  44958  smflimsuplem7  45187  rnghmresfn  46381  rhmresfn  46427  funcringcsetcALTV2lem4  46457  funcringcsetclem4ALTV  46480  rhmsubclem1  46504  rhmsubcALTVlem1  46522  ackvalsucsucval  46894