Theorem fneq1d 6654

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 6652	. 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 6553

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-fun 6560  df-fn 6561

This theorem is used by:  fneq12d  6656  f1o00  6883  f1oprswap  6893  f1ompt  7135  fmpt2d  7149  f1ocnvd  7696  offn  7730  offval2f  7732  offval2  7737  ofrfval2  7738  caofinvl  7749  f1od2  8135  fsplitfpar  8156  omxpenlem  9125  itunifn  10522  konigthlem  10680  seqof  14229  swrdlen  14823  mptfzshft  15973  prdsdsfn  17665  imasdsfn  17715  cidfn  17882  comffn  17908  isoval  17969  invf1o  17973  isofn  17979  brssc  18018  cofucl  18092  estrchomfn  18338  funcestrcsetclem4  18346  funcsetcestrclem4  18361  1stfcl  18400  2ndfcl  18401  prfcl  18406  evlfcl  18425  curf1cl  18431  curfcl  18435  hofcl  18462  yonedainv  18484  smndex1n0mnd  19140  grpinvf1o  19248  ghmquskerco  19528  pmtrrn  19701  pmtrfrn  19702  rnghmresfn  20901  rhmresfn  20930  rhmsubclem1  20967  srngf1o  21135  ofco2  22796  mat1dimscm  22820  neif  23448  fmf  24294  fncpn  26283  mdeg0  26418  om2noseqfo  28714  noseqrdglem  28721  noseqrdgfn  28722  noseqrdg0  28723  tglnfn  29040  tgplnfn  29283  grpoinvf  31164  kbass2  32749  fnresin  33290  f1o3d  33292  suppovss  33345  prodindf  33499  esplyfval3  34274  frlmdim  34313  pstmxmet  34599  ofcfn  34802  ofcfval2  34806  signstlen  35266  bnj941  35473  satfn  36287  msubrn  36461  poimirlem4  38734  cnambfre  38778  sdclem2  38868  diafn  42283  dibfna  42403  dicfnN  42432  dihf11lem  42515  mapd1o  42897  hdmapfnN  43078  hgmapfnN  43137  aks4d1p1p5  43317  hbtlem7  44319  fsovf1od  45208  ntrrn  45314  ntrf  45315  dssmapntrcls  45320  addrfn  45645  subrfn  45646  mulvfn  45647  fsumsermpt  46796  hoidmvlelem3  47812  smflimsuplem7  48041  tmachlem-extpcover  48160  rhmsubcALTVlem1  49583  funcringcsetcALTV2lem4  49595  funcringcsetclem4ALTV  49618  ackvalsucsucval  50005  sectfn  50348  invfn  50349  isofnALT  50350  iinfssclem2  50374  nelsubclem  50386  upeu4  50517  swapf2fn  50595  fucofn2  50651  fucofn22  50667  fucoppc  50750  veronesevrowd  51259  veronesematrowd  51261