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

Theorem fneq2d 5336
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 5334 . 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 1623    Fn wfn 5250
This theorem is referenced by:  fneq12d  5337  undifixp  6852  brwdom2  7287  dfac3  7748  ac7g  8101  ccatlid  11434  ccatrid  11435  ccatass  11436  swrdid  11458  ccatswrd  11459  swrdccat2  11461  revccat  11484  revrev  11485  seqshft  11580  invf  13670  sscfn1  13694  sscfn2  13695  isssc  13697  fuchom  13835  mulgfval  14568  symgplusg  14776  subrgascl  16239  ptval  17265  xpsdsfn2  17942  frlmsslss2  27245  bnj927  28800  dibfnN  31346  dihintcl  31534
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-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fn 5258
  Copyright terms: Public domain W3C validator