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

Theorem fneq2d 5529
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 5527 . 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 1652    Fn wfn 5441
This theorem is referenced by:  fneq12d  5530  undifixp  7090  brwdom2  7533  dfac3  7994  ac7g  8346  ccatlid  11740  ccatrid  11741  ccatass  11742  swrdid  11764  ccatswrd  11765  swrdccat2  11767  revccat  11790  revrev  11791  seqshft  11892  invf  13985  sscfn1  14009  sscfn2  14010  isssc  14012  fuchom  14150  mulgfval  14883  symgplusg  15091  subrgascl  16550  ptval  17594  xpsdsfn2  18400  frlmsslss2  27203  swrd0swrd  28153  swrdswrd  28155  swrdccatin2  28166  swrdccatin12  28170  bnj927  29066  dibfnN  31881  dihintcl  32069
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1551  df-cleq 2428  df-fn 5449
  Copyright terms: Public domain W3C validator