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

Theorem fneq2d 5478
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 5476 . 2  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    = wceq 1649    Fn wfn 5390
This theorem is referenced by:  fneq12d  5479  undifixp  7035  brwdom2  7475  dfac3  7936  ac7g  8288  ccatlid  11676  ccatrid  11677  ccatass  11678  swrdid  11700  ccatswrd  11701  swrdccat2  11703  revccat  11726  revrev  11727  seqshft  11828  invf  13921  sscfn1  13945  sscfn2  13946  isssc  13948  fuchom  14086  mulgfval  14819  symgplusg  15027  subrgascl  16486  ptval  17524  xpsdsfn2  18317  frlmsslss2  26915  bnj927  28478  dibfnN  31272  dihintcl  31460
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2381  df-fn 5398
  Copyright terms: Public domain W3C validator