Theorem predss 6340

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

Step	Hyp	Ref	Expression
1		df-pred 6332	. 2 ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))
2		inss1 4258	. 2 ⊢ (𝐴 ∩ (◡𝑅 “ {𝑋})) ⊆ 𝐴
3	1, 2	eqsstri 4043	1 ⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴

Syntax hints:   ∩ cin 3975   ⊆ wss 3976  {csn 4648  ^◡ccnv 5699   “ cima 5703  Predcpred 6331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993  df-pred 6332

This theorem is referenced by:  frpoins3xpg  8181  frpoins3xp3g  8182  xpord2pred  8186  xpord3pred  8193  fpr3g  8326  frrlem4  8330  frrlem13  8339  fpr1  8344  wfr3g  8363  wfrlem4OLD  8368  wfrlem10OLD  8374  ttrclselem1  9794  frmin  9818  frr3g  9825  frr1  9828  nummin  35067  wsuclem  35789