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

Theorem fneq2d 6597
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 6595 . 2 (𝐴 = 𝐵 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
31, 2syl 17 1 (𝜑 → (𝐹 Fn 𝐴𝐹 Fn 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205   = wceq 1542   Fn wfn 6492
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725  df-fn 6500
This theorem is referenced by:  fneq12d  6598  fncofn  6618  fnco  6619  fnprb  7159  fntpb  7160  fnpr2g  7161  undifixp  8875  brwdom2  9514  brttrcl2  9655  ssttrcl  9656  ttrcltr  9657  ttrclss  9661  ttrclselem2  9667  dfac3  10062  ac7g  10415  ccatlid  14480  ccatrid  14481  ccatass  14482  ccatswrd  14562  swrdccat2  14563  ccatpfx  14595  swrdswrd  14599  swrdccatin2  14623  pfxccatin12  14627  revccat  14660  revrev  14661  repsdf2  14672  0csh0  14687  cshco  14731  wrd2pr2op  14838  wrd3tpop  14843  ofccat  14860  seqshft  14976  invf  17656  sscfn1  17705  sscfn2  17706  isssc  17708  fuchom  17854  fuchomOLD  17855  estrchomfeqhom  18028  mulgfval  18879  mulgfvalALT  18880  frlmsslss2  21197  subrgascl  21490  m1detdiag  21962  ptval  22937  xpsdsfn2  23747  fresf1o  31591  psgndmfi  31996  cycpmconjslem1  32052  cycpmconjslem2  32053  ply1annidllem  32426  pl1cn  32593  signsvtn0  33239  signstres  33244  bnj927  33438  fineqvac  33755  revpfxsfxrev  33766  poimirlem1  36125  poimirlem2  36126  poimirlem3  36127  poimirlem4  36128  poimirlem6  36130  poimirlem7  36131  poimirlem11  36135  poimirlem12  36136  poimirlem16  36140  poimirlem17  36141  poimirlem19  36143  poimirlem20  36144  dibfnN  39665  dihintcl  39853  frlmvscadiccat  40726  ofoafg  41713  uzmptshftfval  42714  srhmsubc  46460  srhmsubcALTV  46478
  Copyright terms: Public domain W3C validator