Theorem fneq1d 6535

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

Syntax hints:   → wi 4   ↔ wb 205   = wceq 1539   Fn wfn 6432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076  df-opab 5138  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-fun 6439  df-fn 6440

This theorem is referenced by:  fneq12d  6537  f1o00  6760  f1oprswap  6769  f1ompt  6994  fmpt2d  7006  f1ocnvd  7529  offn  7555  offval2f  7557  offval2  7562  ofrfval2  7563  caofinvl  7572  fsplitfpar  7968  omxpenlem  8869  itunifn  10182  konigthlem  10333  seqof  13789  swrdlen  14369  mptfzshft  15499  prdsdsfn  17185  imasdsfn  17234  cidfn  17397  comffn  17423  isoval  17486  invf1o  17490  isofn  17496  brssc  17535  cofucl  17612  estrchomfn  17860  funcestrcsetclem4  17869  funcsetcestrclem4  17884  1stfcl  17923  2ndfcl  17924  prfcl  17929  evlfcl  17949  curf1cl  17955  curfcl  17959  hofcl  17986  yonedainv  18008  smndex1n0mnd  18560  grpinvf1o  18654  pmtrrn  19074  pmtrfrn  19075  srngf1o  20123  ofco2  21609  mat1dimscm  21633  neif  22260  fmf  23105  fncpn  25106  mdeg0  25244  tglnfn  26917  grpoinvf  28903  kbass2  30488  fnresin  30970  f1o3d  30971  suppovss  31026  f1od2  31065  frlmdim  31703  pstmxmet  31856  prodindf  32000  ofcfn  32077  ofcfval2  32081  signstlen  32555  bnj941  32761  satfn  33326  msubrn  33500  poimirlem4  35790  cnambfre  35834  sdclem2  35909  diafn  39055  dibfna  39175  dicfnN  39204  dihf11lem  39287  mapd1o  39669  hdmapfnN  39850  hgmapfnN  39909  aks4d1p1p5  40090  hbtlem7  40957  fsovf1od  41631  ntrrn  41739  ntrf  41740  dssmapntrcls  41745  addrfn  42097  subrfn  42098  mulvfn  42099  fsumsermpt  43127  hoidmvlelem3  44142  smflimsuplem7  44370  rnghmresfn  45532  rhmresfn  45578  funcringcsetcALTV2lem4  45608  funcringcsetclem4ALTV  45631  rhmsubclem1  45655  rhmsubcALTVlem1  45673  ackvalsucsucval  46045