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

Theorem fneq1d 5414
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 5412 . 2  |-  ( F  =  G  ->  ( F  Fn  A  <->  G  Fn  A ) )
31, 2syl 15 1  |-  ( ph  ->  ( F  Fn  A  <->  G  Fn  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1642    Fn wfn 5329
This theorem is referenced by:  fneq12d  5416  f1o00  5588  f1oprswap  5595  f1ompt  5762  fmpt2d  5768  f1ocnvd  6150  offn  6173  offval2  6179  ofrfval2  6180  caofinvl  6188  omxpenlem  7048  itunifn  8130  konigthlem  8277  seqof  11192  swrdlen  11546  fsumrev  12332  fsumshft  12333  prdsdsfn  13457  imasdsfn  13510  xpscfn  13554  cidfn  13674  comffn  13701  isoval  13760  invf1o  13764  brssc  13784  cofucl  13855  1stfcl  14064  2ndfcl  14065  prfcl  14070  evlfcl  14089  curf1cl  14095  curfcl  14099  hofcl  14126  yonedainv  14148  grpinvf1o  14631  srngf1o  15712  neif  16937  fmf  17736  fncpn  19380  grpoinvf  21013  kbass2  22805  f1o3d  23242  offval2f  23281  ofcfn  23749  ofcfval2  23753  fprodshft  24601  fprodrev  24602  sdclem2  25776  hbtlem7  26652  pmtrrn  26722  pmtrfrn  26723  addrfn  27000  subrfn  27001  mulvfn  27002  bnj941  28549  diafn  31276  dibfna  31396  dicfnN  31425  dihf11lem  31508  mapd1o  31890  hdmapfnN  32074  hgmapfnN  32133
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-rab 2628  df-v 2866  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-sn 3722  df-pr 3723  df-op 3725  df-br 4103  df-opab 4157  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-fun 5336  df-fn 5337
  Copyright terms: Public domain W3C validator