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

Theorem predss 6262
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 6254 . 2 Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
2 inss1 4189 . 2 (𝐴 ∩ (𝑅 “ {𝑋})) ⊆ 𝐴
31, 2eqsstri 3979 1 Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cin 3910  wss 3911  {csn 4587  ccnv 5633  cima 5637  Predcpred 6253
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-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-pred 6254
This theorem is referenced by:  frpoins3xpg  8073  frpoins3xp3g  8074  xpord2pred  8078  xpord3pred  8085  fpr3g  8217  frrlem4  8221  frrlem13  8230  fpr1  8235  wfr3g  8254  wfrlem4OLD  8259  wfrlem10OLD  8265  ttrclselem1  9666  frmin  9690  frr3g  9697  frr1  9700  nummin  33752  wsuclem  34456
  Copyright terms: Public domain W3C validator