Theorem fneq1d 6624

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 6622	. 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 6526

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-fun 6533  df-fn 6534

This theorem is used by:  fneq12d  6626  f1o00  6852  f1oprswap  6862  f1ompt  7103  fmpt2d  7117  f1ocnvd  7664  offn  7695  offval2f  7697  offval2  7702  ofrfval2  7703  caofinvl  7714  fsplitfpar  8118  omxpenlem  9081  itunifn  10476  konigthlem  10634  seqof  14182  swrdlen  14775  mptfzshft  15924  prdsdsfn  17616  imasdsfn  17666  cidfn  17833  comffn  17859  isoval  17920  invf1o  17924  isofn  17930  brssc  17969  cofucl  18043  estrchomfn  18289  funcestrcsetclem4  18297  funcsetcestrclem4  18312  1stfcl  18351  2ndfcl  18352  prfcl  18357  evlfcl  18376  curf1cl  18382  curfcl  18386  hofcl  18413  yonedainv  18435  smndex1n0mnd  19091  grpinvf1o  19199  ghmquskerco  19478  pmtrrn  19651  pmtrfrn  19652  rnghmresfn  20851  rhmresfn  20880  rhmsubclem1  20917  srngf1o  21085  ofco2  22746  mat1dimscm  22770  neif  23398  fmf  24244  fncpn  26233  mdeg0  26368  om2noseqfo  28666  noseqrdglem  28673  noseqrdgfn  28674  noseqrdg0  28675  tglnfn  28992  tgplnfn  29235  grpoinvf  31116  kbass2  32701  fnresin  33200  f1o3d  33202  suppovss  33256  f1od2  33293  prodindf  33411  esplyfval3  34186  frlmdim  34225  pstmxmet  34511  ofcfn  34714  ofcfval2  34718  signstlen  35179  bnj941  35386  satfn  36089  msubrn  36263  poimirlem4  38510  cnambfre  38554  sdclem2  38644  diafn  42059  dibfna  42179  dicfnN  42208  dihf11lem  42291  mapd1o  42673  hdmapfnN  42854  hgmapfnN  42913  aks4d1p1p5  43093  hbtlem7  44085  fsovf1od  44975  ntrrn  45081  ntrf  45082  dssmapntrcls  45087  addrfn  45413  subrfn  45414  mulvfn  45415  fsumsermpt  46535  hoidmvlelem3  47551  smflimsuplem7  47780  tmachlem-extpcover  47899  rhmsubcALTVlem1  49322  funcringcsetcALTV2lem4  49334  funcringcsetclem4ALTV  49357  ackvalsucsucval  49744  sectfn  50081  invfn  50082  isofnALT  50083  iinfssclem2  50107  nelsubclem  50119  upeu4  50248  swapf2fn  50320  fucofn2  50376  fucofn22  50392  fucoppc  50462  veronesevrowd  50923  veronesematrowd  50925