Theorem fneq1d 6610

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

Syntax hints:   → wi 4   ↔ wb 208   = wceq 1559   Fn wfn 6512

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-rel 5652  df-cnv 5653  df-co 5654  df-dm 5655  df-fun 6519  df-fn 6520

This theorem is referenced by:  fneq12d  6612  f1o00  6838  f1oprswap  6848  f1ompt  7088  fmpt2d  7102  f1ocnvd  7643  offn  7669  offval2f  7671  offval2  7676  ofrfval2  7677  caofinvl  7688  fsplitfpar  8092  omxpenlem  9046  itunifn  10371  konigthlem  10523  seqof  14069  swrdlen  14658  mptfzshft  15788  prdsdsfn  17477  imasdsfn  17527  cidfn  17694  comffn  17720  isoval  17781  invf1o  17785  isofn  17791  brssc  17830  cofucl  17904  estrchomfn  18150  funcestrcsetclem4  18158  funcsetcestrclem4  18173  1stfcl  18212  2ndfcl  18213  prfcl  18218  evlfcl  18237  curf1cl  18243  curfcl  18247  hofcl  18274  yonedainv  18296  smndex1n0mnd  18932  grpinvf1o  19034  ghmquskerco  19307  pmtrrn  19480  pmtrfrn  19481  rnghmresfn  20648  rhmresfn  20677  rhmsubclem1  20714  srngf1o  20877  ofco2  22491  mat1dimscm  22515  neif  23140  fmf  23985  fncpn  25975  mdeg0  26110  om2noseqfo  28368  noseqrdglem  28375  noseqrdgfn  28376  noseqrdg0  28377  tglnfn  28693  grpoinvf  30681  kbass2  32266  fnresin  32776  f1o3d  32778  suppovss  32833  f1od2  32871  prodindf  33001  esplyfval3  33830  frlmdim  33869  pstmxmet  34155  ofcfn  34358  ofcfval2  34362  signstlen  34825  bnj941  35032  satfn  35669  msubrn  35843  poimirlem4  38087  cnambfre  38131  sdclem2  38205  diafn  41622  dibfna  41742  dicfnN  41771  dihf11lem  41854  mapd1o  42236  hdmapfnN  42417  hgmapfnN  42476  aks4d1p1p5  42656  hbtlem7  43666  fsovf1od  44556  ntrrn  44662  ntrf  44663  dssmapntrcls  44668  addrfn  45011  subrfn  45012  mulvfn  45013  fsumsermpt  46119  hoidmvlelem3  47135  smflimsuplem7  47364  rhmsubcALTVlem1  48867  funcringcsetcALTV2lem4  48879  funcringcsetclem4ALTV  48902  ackvalsucsucval  49274  sectfn  49614  invfn  49615  isofnALT  49616  iinfssclem2  49640  nelsubclem  49652  upeu4  49781  swapf2fn  49853  fucofn2  49909  fucofn22  49925  fucoppc  49995