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

Theorem fneq2d 5672
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 5670 . 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 1379    Fn wfn 5583
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5591
This theorem is referenced by:  fneq12d  5673  fnprb  6119  undifixp  7505  brwdom2  7999  dfac3  8502  ac7g  8854  ccatlid  12568  ccatrid  12569  ccatass  12570  swrdid  12615  ccatswrd  12644  swrdccat2  12646  swrdswrd  12648  swrdccatin2  12675  swrdccatin12  12679  revccat  12703  revrev  12704  repsdf2  12713  0csh0  12727  cshco  12765  seqshft  12881  invf  15023  sscfn1  15047  sscfn2  15048  isssc  15050  fuchom  15188  mulgfval  15953  symgplusg  16219  subrgascl  17962  frlmsslss2  18600  frlmsslss2OLD  18601  m1detdiag  18894  ptval  19834  xpsdsfn2  20644  pl1cn  27601  ofccat  28165  signsvtn0  28195  signstres  28200  bnj927  32924  dibfnN  35971  dihintcl  36159
  Copyright terms: Public domain W3C validator