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

Theorem fneq2d 5507
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 5505 . 2  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
31, 2syl 16 1  |-  ( ph  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    Fn wfn 5418
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-fn 5426
This theorem is referenced by:  fneq12d  5508  fnprb  5941  undifixp  7304  brwdom2  7793  dfac3  8296  ac7g  8648  ccatlid  12289  ccatrid  12290  ccatass  12291  swrdid  12326  ccatswrd  12355  swrdccat2  12357  swrdswrd  12359  swrdccatin2  12383  swrdccatin12  12387  revccat  12411  revrev  12412  repsdf2  12421  0csh0  12435  cshco  12469  seqshft  12579  invf  14711  sscfn1  14735  sscfn2  14736  isssc  14738  fuchom  14876  mulgfval  15633  symgplusg  15899  subrgascl  17585  frlmsslss2  18204  frlmsslss2OLD  18205  ptval  19148  xpsdsfn2  19958  pl1cn  26390  ofccat  26946  signsvtn0  26976  signstres  26981  m1detdiag  30939  bnj927  31767  dibfnN  34806  dihintcl  34994
  Copyright terms: Public domain W3C validator