Theorem fneq1d 6611

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

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1540   Fn wfn 6506

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-fun 6513  df-fn 6514

This theorem is referenced by:  fneq12d  6613  f1o00  6835  f1oprswap  6844  f1ompt  7083  fmpt2d  7096  f1ocnvd  7640  offn  7666  offval2f  7668  offval2  7673  ofrfval2  7674  caofinvl  7685  fsplitfpar  8097  omxpenlem  9042  itunifn  10370  konigthlem  10521  seqof  14024  swrdlen  14612  mptfzshft  15744  prdsdsfn  17428  imasdsfn  17477  cidfn  17640  comffn  17666  isoval  17727  invf1o  17731  isofn  17737  brssc  17776  cofucl  17850  estrchomfn  18096  funcestrcsetclem4  18104  funcsetcestrclem4  18119  1stfcl  18158  2ndfcl  18159  prfcl  18164  evlfcl  18183  curf1cl  18189  curfcl  18193  hofcl  18220  yonedainv  18242  smndex1n0mnd  18839  grpinvf1o  18941  ghmquskerco  19216  pmtrrn  19387  pmtrfrn  19388  rnghmresfn  20528  rhmresfn  20557  rhmsubclem1  20594  srngf1o  20757  ofco2  22338  mat1dimscm  22362  neif  22987  fmf  23832  fncpn  25835  mdeg0  25975  om2noseqfo  28192  noseqrdglem  28199  noseqrdgfn  28200  noseqrdg0  28201  tglnfn  28474  grpoinvf  30461  kbass2  32046  fnresin  32550  f1o3d  32551  suppovss  32604  f1od2  32644  prodindf  32786  frlmdim  33607  pstmxmet  33887  ofcfn  34090  ofcfval2  34094  signstlen  34558  bnj941  34762  satfn  35342  msubrn  35516  poimirlem4  37618  cnambfre  37662  sdclem2  37736  diafn  41028  dibfna  41148  dicfnN  41177  dihf11lem  41260  mapd1o  41642  hdmapfnN  41823  hgmapfnN  41882  aks4d1p1p5  42063  hbtlem7  43114  fsovf1od  44005  ntrrn  44111  ntrf  44112  dssmapntrcls  44117  addrfn  44461  subrfn  44462  mulvfn  44463  fsumsermpt  45577  hoidmvlelem3  46595  smflimsuplem7  46824  rhmsubcALTVlem1  48266  funcringcsetcALTV2lem4  48278  funcringcsetclem4ALTV  48301  ackvalsucsucval  48674  sectfn  49015  invfn  49016  isofnALT  49017  iinfssclem2  49041  nelsubclem  49053  upeu4  49182  swapf2fn  49254  fucofn2  49310  fucofn22  49326  fucoppc  49396