Theorem predss 6210

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 6202	. 2 ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋}))
2		inss1 4162	. 2 ⊢ (𝐴 ∩ (◡𝑅 “ {𝑋})) ⊆ 𝐴
3	1, 2	eqsstri 3955	1 ⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴

Syntax hints:   ∩ cin 3886   ⊆ wss 3887  {csn 4561  ^◡ccnv 5588   “ cima 5592  Predcpred 6201

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904  df-pred 6202

This theorem is referenced by:  fpr3g  8101  frrlem4  8105  frrlem13  8114  fpr1  8119  wfr3g  8138  wfrlem4OLD  8143  wfrlem10OLD  8149  ttrclselem1  9483  frmin  9507  frr3g  9514  frr1  9517  nummin  33063  frpoins3xpg  33787  frpoins3xp3g  33788  xpord2pred  33792  xpord3pred  33798  wsuclem  33819