Theorem predss 6303

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

Syntax hints:   ∩ cin 3930   ⊆ wss 3931  {csn 4606  ^◡ccnv 5658   “ cima 5662  Predcpred 6294

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-in 3938  df-ss 3948  df-pred 6295

This theorem is referenced by:  frpoins3xpg  8144  frpoins3xp3g  8145  xpord2pred  8149  xpord3pred  8156  fpr3g  8289  frrlem4  8293  frrlem13  8302  fpr1  8307  wfr3g  8326  wfrlem4OLD  8331  wfrlem10OLD  8337  ttrclselem1  9744  frmin  9768  frr3g  9775  frr1  9778  nummin  35127  wsuclem  35848