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

Theorem fneq1d 5335
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 5333 . 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 1623    Fn wfn 5250
This theorem is referenced by:  fneq12d  5337  f1o00  5508  f1oprswap  5515  f1ompt  5682  fmpt2d  5688  f1ocnvd  6066  offn  6089  offval2  6095  ofrfval2  6096  caofinvl  6104  omxpenlem  6963  itunifn  8043  konigthlem  8190  seqof  11103  swrdlen  11456  fsumrev  12241  fsumshft  12242  prdsdsfn  13364  imasdsfn  13417  xpscfn  13461  cidfn  13581  comffn  13608  isoval  13667  invf1o  13671  brssc  13691  cofucl  13762  1stfcl  13971  2ndfcl  13972  prfcl  13977  evlfcl  13996  curf1cl  14002  curfcl  14006  hofcl  14033  yonedainv  14055  grpinvf1o  14538  srngf1o  15619  neif  16837  fmf  17640  fncpn  19282  grpoinvf  20907  kbass2  22697  f1o3d  23037  offval2f  23233  ofcfn  23461  ofcfval2  23465  npincppr  25159  sdclem2  26452  hbtlem7  27329  pmtrrn  27399  pmtrfrn  27400  addrfn  27677  subrfn  27678  mulvfn  27679  bnj941  28804  diafn  31224  dibfna  31344  dicfnN  31373  dihf11lem  31456  mapd1o  31838  hdmapfnN  32022  hgmapfnN  32081
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-br 4024  df-opab 4078  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-fun 5257  df-fn 5258
  Copyright terms: Public domain W3C validator