Theorem predss 6307

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

Syntax hints:   ∩ cin 3946   ⊆ wss 3947  {csn 4627  ^◡ccnv 5674   “ cima 5678  Predcpred 6298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964  df-pred 6299

This theorem is referenced by:  frpoins3xpg  8128  frpoins3xp3g  8129  xpord2pred  8133  xpord3pred  8140  fpr3g  8272  frrlem4  8276  frrlem13  8285  fpr1  8290  wfr3g  8309  wfrlem4OLD  8314  wfrlem10OLD  8320  ttrclselem1  9722  frmin  9746  frr3g  9753  frr1  9756  nummin  34392  wsuclem  35101