Theorem fneq1d 6635

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 6633	. 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 6538

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 2148  ax-9 2156  ax-ext 2738

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-fun 6545  df-fn 6546

This theorem is used by:  fneq12d  6637  f1o00  6863  f1oprswap  6873  f1ompt  7113  fmpt2d  7127  f1ocnvd  7674  offn  7700  offval2f  7702  offval2  7707  ofrfval2  7708  caofinvl  7719  fsplitfpar  8122  omxpenlem  9076  itunifn  10419  konigthlem  10571  seqof  14115  swrdlen  14707  mptfzshft  15855  prdsdsfn  17543  imasdsfn  17593  cidfn  17760  comffn  17786  isoval  17847  invf1o  17851  isofn  17857  brssc  17896  cofucl  17970  estrchomfn  18216  funcestrcsetclem4  18224  funcsetcestrclem4  18239  1stfcl  18278  2ndfcl  18279  prfcl  18284  evlfcl  18303  curf1cl  18309  curfcl  18313  hofcl  18340  yonedainv  18362  smndex1n0mnd  19005  grpinvf1o  19106  ghmquskerco  19385  pmtrrn  19558  pmtrfrn  19559  rnghmresfn  20755  rhmresfn  20784  rhmsubclem1  20821  srngf1o  20988  ofco2  22645  mat1dimscm  22669  neif  23294  fmf  24139  fncpn  26129  mdeg0  26264  om2noseqfo  28528  noseqrdglem  28535  noseqrdgfn  28536  noseqrdg0  28537  tglnfn  28853  tgplnfn  29094  grpoinvf  30921  kbass2  32506  fnresin  33006  f1o3d  33008  suppovss  33063  f1od2  33101  prodindf  33219  esplyfval3  33993  frlmdim  34032  pstmxmet  34318  ofcfn  34521  ofcfval2  34525  signstlen  34986  bnj941  35193  satfn  35868  msubrn  36042  poimirlem4  38316  cnambfre  38360  sdclem2  38434  diafn  41849  dibfna  41969  dicfnN  41998  dihf11lem  42081  mapd1o  42463  hdmapfnN  42644  hgmapfnN  42703  aks4d1p1p5  42883  hbtlem7  43893  fsovf1od  44783  ntrrn  44889  ntrf  44890  dssmapntrcls  44895  addrfn  45221  subrfn  45222  mulvfn  45223  fsumsermpt  46336  hoidmvlelem3  47352  smflimsuplem7  47581  rhmsubcALTVlem1  49087  funcringcsetcALTV2lem4  49099  funcringcsetclem4ALTV  49122  ackvalsucsucval  49509  sectfn  49848  invfn  49849  isofnALT  49850  iinfssclem2  49874  nelsubclem  49886  upeu4  50015  swapf2fn  50087  fucofn2  50143  fucofn22  50159  fucoppc  50229