Theorem fneq1d 5981

Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
fneq1d.1	|- ( ph -> F = G )

Assertion

Ref	Expression
fneq1d	|- ( ph -> ( F Fn A <-> G Fn A ) )

Proof of Theorem fneq1d

Step	Hyp	Ref	Expression
1		fneq1d.1	. 2 |- ( ph -> F = G )
2		fneq1 5979	. 2 |- ( F = G -> ( F Fn A <-> G Fn A ) )
3	1, 2	syl 17	1 |- ( ph -> ( F Fn A <-> G Fn A ) )

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   Fn wfn 5883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-fun 5890  df-fn 5891

This theorem is referenced by:  fneq12d  5983  f1o00  6171  f1oprswap  6180  f1ompt  6382  fmpt2d  6393  f1ocnvd  6884  offn  6908  offval2f  6909  offval2  6914  ofrfval2  6915  caofinvl  6924  suppsnop  7309  omxpenlem  8061  itunifn  9239  konigthlem  9390  seqof  12858  swrdlen  13423  mptfzshft  14510  fsumrev  14511  fprodrev  14707  prdsdsfn  16125  imasdsfn  16174  xpscfn  16219  cidfn  16340  comffn  16365  isoval  16425  invf1o  16429  isofn  16435  brssc  16474  cofucl  16548  estrchomfn  16775  funcestrcsetclem4  16783  funcsetcestrclem4  16798  1stfcl  16837  2ndfcl  16838  prfcl  16843  evlfcl  16862  curf1cl  16868  curfcl  16872  hofcl  16899  yonedainv  16921  grpinvf1o  17485  pmtrrn  17877  pmtrfrn  17878  srngf1o  18854  ofco2  20257  mat1dimscm  20281  neif  20904  fmf  21749  fncpn  23696  mdeg0  23830  tglnfn  25442  grpoinvf  27386  kbass2  28976  fnresin  29430  f1o3d  29431  f1od2  29499  pstmxmet  29940  prodindf  30085  ofcfn  30162  ofcfval2  30166  signstlen  30644  bnj941  30843  msubrn  31426  poimirlem4  33413  cnambfre  33458  sdclem2  33538  diafn  36323  dibfna  36443  dicfnN  36472  dihf11lem  36555  mapd1o  36937  hdmapfnN  37121  hgmapfnN  37180  hbtlem7  37695  fsovf1od  38310  ntrrn  38420  ntrf  38421  dssmapntrcls  38426  addrfn  38676  subrfn  38677  mulvfn  38678  fsumsermpt  39811  hoidmvlelem3  40811  smflimsuplem7  41032  rnghmresfn  41963  rhmresfn  42009  funcringcsetcALTV2lem4  42039  funcringcsetclem4ALTV  42062  rhmsubclem1  42086  rhmsubcALTVlem1  42104