Theorem fneq1d 6579

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1541   Fn wfn 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-fun 6488  df-fn 6489

This theorem is referenced by:  fneq12d  6581  f1o00  6803  f1oprswap  6813  f1ompt  7050  fmpt2d  7063  f1ocnvd  7603  offn  7629  offval2f  7631  offval2  7636  ofrfval2  7637  caofinvl  7648  fsplitfpar  8054  omxpenlem  8998  itunifn  10315  konigthlem  10466  seqof  13968  swrdlen  14557  mptfzshft  15687  prdsdsfn  17371  imasdsfn  17420  cidfn  17587  comffn  17613  isoval  17674  invf1o  17678  isofn  17684  brssc  17723  cofucl  17797  estrchomfn  18043  funcestrcsetclem4  18051  funcsetcestrclem4  18066  1stfcl  18105  2ndfcl  18106  prfcl  18111  evlfcl  18130  curf1cl  18136  curfcl  18140  hofcl  18167  yonedainv  18189  smndex1n0mnd  18822  grpinvf1o  18924  ghmquskerco  19198  pmtrrn  19371  pmtrfrn  19372  rnghmresfn  20536  rhmresfn  20565  rhmsubclem1  20602  srngf1o  20765  ofco2  22367  mat1dimscm  22391  neif  23016  fmf  23861  fncpn  25863  mdeg0  26003  om2noseqfo  28229  noseqrdglem  28236  noseqrdgfn  28237  noseqrdg0  28238  tglnfn  28526  grpoinvf  30514  kbass2  32099  fnresin  32609  f1o3d  32610  suppovss  32666  f1od2  32706  prodindf  32851  esplyfval3  33612  frlmdim  33645  pstmxmet  33931  ofcfn  34134  ofcfval2  34138  signstlen  34601  bnj941  34805  satfn  35420  msubrn  35594  poimirlem4  37685  cnambfre  37729  sdclem2  37803  diafn  41154  dibfna  41274  dicfnN  41303  dihf11lem  41386  mapd1o  41768  hdmapfnN  41949  hgmapfnN  42008  aks4d1p1p5  42189  hbtlem7  43243  fsovf1od  44134  ntrrn  44240  ntrf  44241  dssmapntrcls  44246  addrfn  44589  subrfn  44590  mulvfn  44591  fsumsermpt  45704  hoidmvlelem3  46720  smflimsuplem7  46949  rhmsubcALTVlem1  48406  funcringcsetcALTV2lem4  48418  funcringcsetclem4ALTV  48441  ackvalsucsucval  48814  sectfn  49155  invfn  49156  isofnALT  49157  iinfssclem2  49181  nelsubclem  49193  upeu4  49322  swapf2fn  49394  fucofn2  49450  fucofn22  49466  fucoppc  49536