MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fneq1d Structured version   Unicode version

Theorem fneq1d 5599
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
StepHypRef Expression
1 fneq1d.1 . 2  |-  ( ph  ->  F  =  G )
2 fneq1 5597 . 2  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
31, 2syl 16 1  |-  ( ph  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1370    Fn wfn 5511
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-rab 2804  df-v 3070  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-sn 3976  df-pr 3978  df-op 3982  df-br 4391  df-opab 4449  df-rel 4945  df-cnv 4946  df-co 4947  df-dm 4948  df-fun 5518  df-fn 5519
This theorem is referenced by:  fneq12d  5601  f1o00  5771  f1oprswap  5778  f1ompt  5964  fmpt2d  5972  f1ocnvd  6409  offn  6431  offval2  6436  ofrfval2  6437  caofinvl  6447  suppsnop  6804  omxpenlem  7512  itunifn  8687  konigthlem  8833  seqof  11964  swrdlen  12421  mptfzshft  13347  fsumrev  13348  prdsdsfn  14505  imasdsfn  14554  xpscfn  14599  cidfn  14719  comffn  14746  isoval  14805  invf1o  14809  brssc  14829  cofucl  14900  1stfcl  15109  2ndfcl  15110  prfcl  15115  evlfcl  15134  curf1cl  15140  curfcl  15144  hofcl  15171  yonedainv  15193  grpinvf1o  15698  pmtrrn  16065  pmtrfrn  16066  srngf1o  17045  ofco2  18443  neif  18820  fmf  19634  fncpn  21523  mdeg0  21657  tglnfn  23100  grpoinvf  23862  kbass2  25656  fnresin  26081  f1o3d  26082  offval2f  26117  f1od2  26158  pstmxmet  26458  ofcfn  26676  ofcfval2  26680  signstlen  27102  fprodshft  27621  fprodrev  27622  cnambfre  28578  sdclem2  28776  hbtlem7  29619  addrfn  29866  subrfn  29867  mulvfn  29868  mat1dimscm  31025  bnj941  32066  diafn  34985  dibfna  35105  dicfnN  35134  dihf11lem  35217  mapd1o  35599  hdmapfnN  35783  hgmapfnN  35842
  Copyright terms: Public domain W3C validator