Theorem fneq1d 6642

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

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

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 2703

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 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-fun 6545  df-fn 6546

This theorem is referenced by:  fneq12d  6644  f1o00  6868  f1oprswap  6877  f1ompt  7112  fmpt2d  7125  f1ocnvd  7659  offn  7685  offval2f  7687  offval2  7692  ofrfval2  7693  caofinvl  7702  fsplitfpar  8106  omxpenlem  9075  itunifn  10414  konigthlem  10565  seqof  14029  swrdlen  14601  mptfzshft  15728  prdsdsfn  17415  imasdsfn  17464  cidfn  17627  comffn  17653  isoval  17716  invf1o  17720  isofn  17726  brssc  17765  cofucl  17842  estrchomfn  18090  funcestrcsetclem4  18099  funcsetcestrclem4  18114  1stfcl  18153  2ndfcl  18154  prfcl  18159  evlfcl  18179  curf1cl  18185  curfcl  18189  hofcl  18216  yonedainv  18238  smndex1n0mnd  18829  grpinvf1o  18929  pmtrrn  19366  pmtrfrn  19367  srngf1o  20605  ofco2  22173  mat1dimscm  22197  neif  22824  fmf  23669  fncpn  25674  mdeg0  25812  tglnfn  28053  grpoinvf  30040  kbass2  31625  fnresin  32105  f1o3d  32106  suppovss  32161  f1od2  32201  ghmquskerco  32791  frlmdim  32972  pstmxmet  33163  prodindf  33307  ofcfn  33384  ofcfval2  33388  signstlen  33864  bnj941  34069  satfn  34632  msubrn  34806  poimirlem4  36795  cnambfre  36839  sdclem2  36913  diafn  40208  dibfna  40328  dicfnN  40357  dihf11lem  40440  mapd1o  40822  hdmapfnN  41003  hgmapfnN  41062  aks4d1p1p5  41246  hbtlem7  42169  fsovf1od  43069  ntrrn  43175  ntrf  43176  dssmapntrcls  43181  addrfn  43533  subrfn  43534  mulvfn  43535  fsumsermpt  44594  hoidmvlelem3  45612  smflimsuplem7  45841  rnghmresfn  46950  rhmresfn  46996  funcringcsetcALTV2lem4  47026  funcringcsetclem4ALTV  47049  rhmsubclem1  47073  rhmsubcALTVlem1  47091  ackvalsucsucval  47462