Theorem fneq1d 6660

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1539   Fn wfn 6555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143  df-opab 5205  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-fun 6562  df-fn 6563

This theorem is referenced by:  fneq12d  6662  f1o00  6882  f1oprswap  6891  f1ompt  7130  fmpt2d  7143  f1ocnvd  7685  offn  7711  offval2f  7713  offval2  7718  ofrfval2  7719  caofinvl  7730  fsplitfpar  8144  omxpenlem  9114  itunifn  10458  konigthlem  10609  seqof  14101  swrdlen  14686  mptfzshft  15815  prdsdsfn  17511  imasdsfn  17560  cidfn  17723  comffn  17749  isoval  17810  invf1o  17814  isofn  17820  brssc  17859  cofucl  17934  estrchomfn  18180  funcestrcsetclem4  18189  funcsetcestrclem4  18204  1stfcl  18243  2ndfcl  18244  prfcl  18249  evlfcl  18268  curf1cl  18274  curfcl  18278  hofcl  18305  yonedainv  18327  smndex1n0mnd  18926  grpinvf1o  19028  ghmquskerco  19303  pmtrrn  19476  pmtrfrn  19477  rnghmresfn  20620  rhmresfn  20649  rhmsubclem1  20686  srngf1o  20850  ofco2  22458  mat1dimscm  22482  neif  23109  fmf  23954  fncpn  25970  mdeg0  26110  om2noseqfo  28305  noseqrdglem  28312  noseqrdgfn  28313  noseqrdg0  28314  tglnfn  28556  grpoinvf  30552  kbass2  32137  fnresin  32637  f1o3d  32638  suppovss  32691  f1od2  32733  prodindf  32849  frlmdim  33663  pstmxmet  33897  ofcfn  34102  ofcfval2  34106  signstlen  34583  bnj941  34787  satfn  35361  msubrn  35535  poimirlem4  37632  cnambfre  37676  sdclem2  37750  diafn  41037  dibfna  41157  dicfnN  41186  dihf11lem  41269  mapd1o  41651  hdmapfnN  41832  hgmapfnN  41891  aks4d1p1p5  42077  hbtlem7  43142  fsovf1od  44034  ntrrn  44140  ntrf  44141  dssmapntrcls  44146  addrfn  44496  subrfn  44497  mulvfn  44498  fsumsermpt  45599  hoidmvlelem3  46617  smflimsuplem7  46846  rhmsubcALTVlem1  48202  funcringcsetcALTV2lem4  48214  funcringcsetclem4ALTV  48237  ackvalsucsucval  48614  upeu4  48965  swapf2fn  48992  fucofn2  49042  fucofn22  49058