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

Theorem predss 6308
Description: The predecessor class of 𝐴 is a subset of 𝐴. (Contributed by Scott Fenton, 2-Feb-2011.)
Assertion
Ref Expression
predss Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴

Proof of Theorem predss
StepHypRef Expression
1 df-pred 6300 . 2 Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
2 inss1 4228 . 2 (𝐴 ∩ (𝑅 “ {𝑋})) ⊆ 𝐴
31, 2eqsstri 4016 1 Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cin 3947  wss 3948  {csn 4628  ccnv 5675  cima 5679  Predcpred 6299
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-pred 6300
This theorem is referenced by:  frpoins3xpg  8125  frpoins3xp3g  8126  xpord2pred  8130  xpord3pred  8137  fpr3g  8269  frrlem4  8273  frrlem13  8282  fpr1  8287  wfr3g  8306  wfrlem4OLD  8311  wfrlem10OLD  8317  ttrclselem1  9719  frmin  9743  frr3g  9750  frr1  9753  nummin  34089  wsuclem  34792
  Copyright terms: Public domain W3C validator