|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > predss | Structured version Visualization version GIF version | ||
| Description: The predecessor class of 𝐴 is a subset of 𝐴. (Contributed by Scott Fenton, 2-Feb-2011.) | 
| Ref | Expression | 
|---|---|
| predss | ⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴 | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | df-pred 6321 | . 2 ⊢ Pred(𝑅, 𝐴, 𝑋) = (𝐴 ∩ (◡𝑅 “ {𝑋})) | |
| 2 | inss1 4237 | . 2 ⊢ (𝐴 ∩ (◡𝑅 “ {𝑋})) ⊆ 𝐴 | |
| 3 | 1, 2 | eqsstri 4030 | 1 ⊢ Pred(𝑅, 𝐴, 𝑋) ⊆ 𝐴 | 
| Colors of variables: wff setvar class | 
| Syntax hints: ∩ cin 3950 ⊆ wss 3951 {csn 4626 ◡ccnv 5684 “ cima 5688 Predcpred 6320 | 
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-ss 3968 df-pred 6321 | 
| This theorem is referenced by: frpoins3xpg 8165 frpoins3xp3g 8166 xpord2pred 8170 xpord3pred 8177 fpr3g 8310 frrlem4 8314 frrlem13 8323 fpr1 8328 wfr3g 8347 wfrlem4OLD 8352 wfrlem10OLD 8358 ttrclselem1 9765 frmin 9789 frr3g 9796 frr1 9799 nummin 35105 wsuclem 35826 | 
| Copyright terms: Public domain | W3C validator |