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

Theorem predss 6328
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 6320 . 2 Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (𝑅 “ {𝑋}))
2 inss1 4236 . 2 (𝐴 ∩ (𝑅 “ {𝑋})) ⊆ 𝐴
31, 2eqsstri 4029 1 Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴
Colors of variables: wff setvar class
Syntax hints:  cin 3949  wss 3950  {csn 4625  ccnv 5683  cima 5687  Predcpred 6319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-in 3957  df-ss 3967  df-pred 6320
This theorem is referenced by:  frpoins3xpg  8166  frpoins3xp3g  8167  xpord2pred  8171  xpord3pred  8178  fpr3g  8311  frrlem4  8315  frrlem13  8324  fpr1  8329  wfr3g  8348  wfrlem4OLD  8353  wfrlem10OLD  8359  ttrclselem1  9766  frmin  9790  frr3g  9797  frr1  9800  nummin  35106  wsuclem  35827
  Copyright terms: Public domain W3C validator