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

Theorem fneq2d 5896
 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 5894 . 2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   = wceq 1475   Fn wfn 5799 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603  df-fn 5807 This theorem is referenced by:  fneq12d  5897  fnprb  6377  fntpb  6378  fnpr2g  6379  undifixp  7830  brwdom2  8361  dfac3  8827  ac7g  9179  ccatlid  13222  ccatrid  13223  ccatass  13224  ccatswrd  13308  swrdccat2  13310  swrdswrd  13312  swrdccatin2  13338  swrdccatin12  13342  revccat  13366  revrev  13367  repsdf2  13376  0csh0  13390  cshco  13433  wrd2pr2op  13535  wrd3tpop  13539  ofccat  13556  seqshft  13673  invf  16251  sscfn1  16300  sscfn2  16301  isssc  16303  fuchom  16444  estrchomfeqhom  16599  mulgfval  17365  symgplusg  17632  subrgascl  19319  frlmsslss2  19933  m1detdiag  20222  ptval  21183  xpsdsfn2  21993  fresf1o  28815  psgndmfi  29177  pl1cn  29329  signsvtn0  29973  signstres  29978  bnj927  30093  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  dibfnN  35463  dihintcl  35651  uzmptshftfval  37567  ccatpfx  40272  pfxccatin12  40288  srhmsubc  41868  srhmsubcALTV  41887
 Copyright terms: Public domain W3C validator