Theorem fneq1d 6591

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-fun 6500  df-fn 6501

This theorem is referenced by:  fneq12d  6593  f1o00  6815  f1oprswap  6825  f1ompt  7063  fmpt2d  7077  f1ocnvd  7618  offn  7644  offval2f  7646  offval2  7651  ofrfval2  7652  caofinvl  7663  fsplitfpar  8068  omxpenlem  9016  itunifn  10339  konigthlem  10491  seqof  14021  swrdlen  14610  mptfzshft  15740  prdsdsfn  17428  imasdsfn  17478  cidfn  17645  comffn  17671  isoval  17732  invf1o  17736  isofn  17742  brssc  17781  cofucl  17855  estrchomfn  18101  funcestrcsetclem4  18109  funcsetcestrclem4  18124  1stfcl  18163  2ndfcl  18164  prfcl  18169  evlfcl  18188  curf1cl  18194  curfcl  18198  hofcl  18225  yonedainv  18247  smndex1n0mnd  18883  grpinvf1o  18985  ghmquskerco  19259  pmtrrn  19432  pmtrfrn  19433  rnghmresfn  20596  rhmresfn  20625  rhmsubclem1  20662  srngf1o  20825  ofco2  22416  mat1dimscm  22440  neif  23065  fmf  23910  fncpn  25900  mdeg0  26035  om2noseqfo  28290  noseqrdglem  28297  noseqrdgfn  28298  noseqrdg0  28299  tglnfn  28615  grpoinvf  30603  kbass2  32188  fnresin  32697  f1o3d  32699  suppovss  32754  f1od2  32792  prodindf  32922  esplyfval3  33716  frlmdim  33755  pstmxmet  34041  ofcfn  34244  ofcfval2  34248  signstlen  34711  bnj941  34915  satfn  35537  msubrn  35711  poimirlem4  37945  cnambfre  37989  sdclem2  38063  diafn  41480  dibfna  41600  dicfnN  41629  dihf11lem  41712  mapd1o  42094  hdmapfnN  42275  hgmapfnN  42334  aks4d1p1p5  42514  hbtlem7  43553  fsovf1od  44443  ntrrn  44549  ntrf  44550  dssmapntrcls  44555  addrfn  44898  subrfn  44899  mulvfn  44900  fsumsermpt  46009  hoidmvlelem3  47025  smflimsuplem7  47254  rhmsubcALTVlem1  48757  funcringcsetcALTV2lem4  48769  funcringcsetclem4ALTV  48792  ackvalsucsucval  49164  sectfn  49504  invfn  49505  isofnALT  49506  iinfssclem2  49530  nelsubclem  49542  upeu4  49671  swapf2fn  49743  fucofn2  49799  fucofn22  49815  fucoppc  49885