Theorem predss 6316

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

Syntax hints:   ∩ cin 3946   ⊆ wss 3947  {csn 4630  ^◡ccnv 5679   “ cima 5683  Predcpred 6307

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3473  df-in 3954  df-ss 3964  df-pred 6308

This theorem is referenced by:  frpoins3xpg  8149  frpoins3xp3g  8150  xpord2pred  8154  xpord3pred  8161  fpr3g  8295  frrlem4  8299  frrlem13  8308  fpr1  8313  wfr3g  8332  wfrlem4OLD  8337  wfrlem10OLD  8343  ttrclselem1  9754  frmin  9778  frr3g  9785  frr1  9788  nummin  34719  wsuclem  35426