Theorem fneq1d 6630

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

Syntax hints:   → wi 4   ↔ wb 209   = wceq 1570   Fn wfn 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-fun 6540  df-fn 6541

This theorem is referenced by:  fneq12d  6632  f1o00  6858  f1oprswap  6868  f1ompt  7108  fmpt2d  7122  f1ocnvd  7663  offn  7689  offval2f  7691  offval2  7696  ofrfval2  7697  caofinvl  7708  fsplitfpar  8114  omxpenlem  9067  itunifn  10402  konigthlem  10554  seqof  14097  swrdlen  14687  mptfzshft  15831  prdsdsfn  17519  imasdsfn  17569  cidfn  17736  comffn  17762  isoval  17823  invf1o  17827  isofn  17833  brssc  17872  cofucl  17946  estrchomfn  18192  funcestrcsetclem4  18200  funcsetcestrclem4  18215  1stfcl  18254  2ndfcl  18255  prfcl  18260  evlfcl  18279  curf1cl  18285  curfcl  18289  hofcl  18316  yonedainv  18338  smndex1n0mnd  18975  grpinvf1o  19076  ghmquskerco  19355  pmtrrn  19528  pmtrfrn  19529  rnghmresfn  20705  rhmresfn  20734  rhmsubclem1  20771  srngf1o  20932  ofco2  22589  mat1dimscm  22613  neif  23238  fmf  24083  fncpn  26073  mdeg0  26208  om2noseqfo  28469  noseqrdglem  28476  noseqrdgfn  28477  noseqrdg0  28478  tglnfn  28794  tgplnfn  29035  grpoinvf  30862  kbass2  32447  fnresin  32947  f1o3d  32949  suppovss  33004  f1od2  33042  prodindf  33160  esplyfval3  33940  frlmdim  33979  pstmxmet  34265  ofcfn  34468  ofcfval2  34472  signstlen  34932  bnj941  35139  satfn  35825  msubrn  35999  poimirlem4  38253  cnambfre  38297  sdclem2  38371  diafn  41786  dibfna  41906  dicfnN  41935  dihf11lem  42018  mapd1o  42400  hdmapfnN  42581  hgmapfnN  42640  aks4d1p1p5  42820  hbtlem7  43832  fsovf1od  44722  ntrrn  44828  ntrf  44829  dssmapntrcls  44834  addrfn  45160  subrfn  45161  mulvfn  45162  fsumsermpt  46275  hoidmvlelem3  47291  smflimsuplem7  47520  rhmsubcALTVlem1  49023  funcringcsetcALTV2lem4  49035  funcringcsetclem4ALTV  49058  ackvalsucsucval  49445  sectfn  49784  invfn  49785  isofnALT  49786  iinfssclem2  49810  nelsubclem  49822  upeu4  49951  swapf2fn  50023  fucofn2  50079  fucofn22  50095  fucoppc  50165