Theorem fneq1d 6629

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   = wceq 1570   Fn wfn 6532

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108  df-opab 5172  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-fun 6539  df-fn 6540

This theorem is used by:  fneq12d  6631  f1o00  6857  f1oprswap  6867  f1ompt  7108  fmpt2d  7122  f1ocnvd  7669  offn  7695  offval2f  7697  offval2  7702  ofrfval2  7703  caofinvl  7714  fsplitfpar  8119  omxpenlem  9080  itunifn  10423  konigthlem  10581  seqof  14127  swrdlen  14719  mptfzshft  15868  prdsdsfn  17556  imasdsfn  17606  cidfn  17773  comffn  17799  isoval  17860  invf1o  17864  isofn  17870  brssc  17909  cofucl  17983  estrchomfn  18229  funcestrcsetclem4  18237  funcsetcestrclem4  18252  1stfcl  18291  2ndfcl  18292  prfcl  18297  evlfcl  18316  curf1cl  18322  curfcl  18326  hofcl  18353  yonedainv  18375  smndex1n0mnd  19030  grpinvf1o  19138  ghmquskerco  19417  pmtrrn  19590  pmtrfrn  19591  rnghmresfn  20787  rhmresfn  20816  rhmsubclem1  20853  srngf1o  21020  ofco2  22679  mat1dimscm  22703  neif  23331  fmf  24177  fncpn  26167  mdeg0  26302  om2noseqfo  28571  noseqrdglem  28578  noseqrdgfn  28579  noseqrdg0  28580  tglnfn  28897  tgplnfn  29140  grpoinvf  31021  kbass2  32606  fnresin  33105  f1o3d  33107  suppovss  33161  f1od2  33198  prodindf  33316  esplyfval3  34090  frlmdim  34129  pstmxmet  34415  ofcfn  34618  ofcfval2  34622  signstlen  35083  bnj941  35290  satfn  35942  msubrn  36116  poimirlem4  38381  cnambfre  38425  sdclem2  38500  diafn  41915  dibfna  42035  dicfnN  42064  dihf11lem  42147  mapd1o  42529  hdmapfnN  42710  hgmapfnN  42769  aks4d1p1p5  42949  hbtlem7  43974  fsovf1od  44864  ntrrn  44970  ntrf  44971  dssmapntrcls  44976  addrfn  45302  subrfn  45303  mulvfn  45304  fsumsermpt  46417  hoidmvlelem3  47433  smflimsuplem7  47662  tmachlem-extpcover  47781  rhmsubcALTVlem1  49204  funcringcsetcALTV2lem4  49216  funcringcsetclem4ALTV  49239  ackvalsucsucval  49626  sectfn  49963  invfn  49964  isofnALT  49965  iinfssclem2  49989  nelsubclem  50001  upeu4  50130  swapf2fn  50202  fucofn2  50258  fucofn22  50274  fucoppc  50344  veronesevrowd  50820  veronesematrowd  50822