Theorem fneq1d 6585

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

Syntax hints:   → wi 4   ↔ wb 207   = wceq 1547   Fn wfn 6487

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-fun 6494  df-fn 6495

This theorem is referenced by:  fneq12d  6587  f1o00  6809  f1oprswap  6819  f1ompt  7059  fmpt2d  7073  f1ocnvd  7614  offn  7640  offval2f  7642  offval2  7647  ofrfval2  7648  caofinvl  7659  fsplitfpar  8064  omxpenlem  9013  itunifn  10337  konigthlem  10489  seqof  14019  swrdlen  14608  mptfzshft  15738  prdsdsfn  17426  imasdsfn  17476  cidfn  17643  comffn  17669  isoval  17730  invf1o  17734  isofn  17740  brssc  17779  cofucl  17853  estrchomfn  18099  funcestrcsetclem4  18107  funcsetcestrclem4  18122  1stfcl  18161  2ndfcl  18162  prfcl  18167  evlfcl  18186  curf1cl  18192  curfcl  18196  hofcl  18223  yonedainv  18245  smndex1n0mnd  18881  grpinvf1o  18983  ghmquskerco  19257  pmtrrn  19430  pmtrfrn  19431  rnghmresfn  20598  rhmresfn  20627  rhmsubclem1  20664  srngf1o  20827  ofco2  22441  mat1dimscm  22465  neif  23090  fmf  23935  fncpn  25925  mdeg0  26060  om2noseqfo  28315  noseqrdglem  28322  noseqrdgfn  28323  noseqrdg0  28324  tglnfn  28640  grpoinvf  30628  kbass2  32213  fnresin  32723  f1o3d  32725  suppovss  32780  f1od2  32818  prodindf  32948  esplyfval3  33763  frlmdim  33802  pstmxmet  34088  ofcfn  34291  ofcfval2  34295  signstlen  34758  bnj941  34962  satfn  35590  msubrn  35764  poimirlem4  37998  cnambfre  38042  sdclem2  38116  diafn  41533  dibfna  41653  dicfnN  41682  dihf11lem  41765  mapd1o  42147  hdmapfnN  42328  hgmapfnN  42387  aks4d1p1p5  42567  hbtlem7  43577  fsovf1od  44467  ntrrn  44573  ntrf  44574  dssmapntrcls  44579  addrfn  44922  subrfn  44923  mulvfn  44924  fsumsermpt  46031  hoidmvlelem3  47047  smflimsuplem7  47276  rhmsubcALTVlem1  48779  funcringcsetcALTV2lem4  48791  funcringcsetclem4ALTV  48814  ackvalsucsucval  49186  sectfn  49526  invfn  49527  isofnALT  49528  iinfssclem2  49552  nelsubclem  49564  upeu4  49693  swapf2fn  49765  fucofn2  49821  fucofn22  49837  fucoppc  49907