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

Theorem fneq2d 5685
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 5683 . 2  |-  ( A  =  B  ->  ( F  Fn  A  <->  F  Fn  B ) )
31, 2syl 17 1  |-  ( ph  ->  ( F  Fn  A  <->  F  Fn  B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    = wceq 1437    Fn wfn 5596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421  df-fn 5604
This theorem is referenced by:  fneq12d  5686  fnprb  6138  fnpr2g  6139  undifixp  7566  brwdom2  8088  dfac3  8550  ac7g  8902  ccatlid  12717  ccatrid  12718  ccatass  12719  ccatswrd  12797  swrdccat2  12799  swrdswrd  12801  swrdccatin2  12828  swrdccatin12  12832  revccat  12856  revrev  12857  repsdf2  12866  0csh0  12880  cshco  12918  seqshft  13127  invf  15624  sscfn1  15673  sscfn2  15674  isssc  15676  fuchom  15817  estrchomfeqhom  15972  mulgfval  16710  symgplusg  16981  subrgascl  18656  frlmsslss2  19264  m1detdiag  19553  ptval  20516  xpsdsfn2  21324  fresf1o  28071  psgndmfi  28448  pl1cn  28600  ofccat  29217  signsvtn0  29247  signstres  29252  bnj927  29368  poimirlem1  31645  poimirlem2  31646  poimirlem3  31647  poimirlem4  31648  poimirlem6  31650  poimirlem7  31651  poimirlem11  31655  poimirlem12  31656  poimirlem16  31660  poimirlem17  31661  poimirlem19  31663  poimirlem20  31664  dibfnN  34433  dihintcl  34621  uzmptshftfval  36332  ccatpfx  38349  pfxccatin12  38365  srhmsubc  38845  srhmsubcALTV  38864
  Copyright terms: Public domain W3C validator