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

Theorem fneq2d 5352
Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq2d.1  |-  ( ph  ->  A  =  B )
Assertion
Ref Expression
fneq2d  |-  ( ph  ->  ( F  Fn  A  <->  F  Fn  B ) )

Proof of Theorem fneq2d
StepHypRef Expression
1 fneq2d.1 . 2  |-  ( ph  ->  A  =  B )
2 fneq2 5350 . 2  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
31, 2syl 15 1  |-  ( ph  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    = wceq 1632    Fn wfn 5266
This theorem is referenced by:  fneq12d  5353  undifixp  6868  brwdom2  7303  dfac3  7764  ac7g  8117  ccatlid  11450  ccatrid  11451  ccatass  11452  swrdid  11474  ccatswrd  11475  swrdccat2  11477  revccat  11500  revrev  11501  seqshft  11596  invf  13686  sscfn1  13710  sscfn2  13711  isssc  13713  fuchom  13851  mulgfval  14584  symgplusg  14792  subrgascl  16255  ptval  17281  xpsdsfn2  17958  frlmsslss2  27348  bnj927  29116  dibfnN  31968  dihintcl  32156
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289  df-fn 5274
  Copyright terms: Public domain W3C validator