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

Theorem fneq2d 5970
Description: Equality deduction for function predicate with domain. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
fneq2d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
fneq2d (𝜑 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))

Proof of Theorem fneq2d
StepHypRef Expression
1 fneq2d.1 . 2 (𝜑𝐴 = 𝐵)
2 fneq2 5968 . 2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1481   Fn wfn 5871
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613  df-fn 5879
This theorem is referenced by:  fneq12d  5971  fnprb  6457  fntpb  6458  fnpr2g  6459  undifixp  7929  brwdom2  8463  dfac3  8929  ac7g  9281  ccatlid  13352  ccatrid  13353  ccatass  13354  ccatswrd  13438  swrdccat2  13440  swrdswrd  13442  swrdccatin2  13468  swrdccatin12  13472  revccat  13496  revrev  13497  repsdf2  13506  0csh0  13520  cshco  13563  wrd2pr2op  13668  wrd3tpop  13672  ofccat  13689  seqshft  13806  invf  16409  sscfn1  16458  sscfn2  16459  isssc  16461  fuchom  16602  estrchomfeqhom  16757  mulgfval  17523  symgplusg  17790  subrgascl  19479  frlmsslss2  20095  m1detdiag  20384  ptval  21354  xpsdsfn2  22164  fresf1o  29406  psgndmfi  29820  pl1cn  29975  signsvtn0  30621  signstres  30626  bnj927  30813  poimirlem1  33381  poimirlem2  33382  poimirlem3  33383  poimirlem4  33384  poimirlem6  33386  poimirlem7  33387  poimirlem11  33391  poimirlem12  33392  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  dibfnN  36264  dihintcl  36452  uzmptshftfval  38365  ccatpfx  41174  pfxccatin12  41190  srhmsubc  41841  srhmsubcALTV  41859
  Copyright terms: Public domain W3C validator