Metamath Proof Explorer


Theorem predss

Description: The predecessor class of A is a subset of A . (Contributed by Scott Fenton, 2-Feb-2011)

Ref Expression
Assertion predss PredRAXA

Proof

Step Hyp Ref Expression
1 df-pred PredRAX=AR-1X
2 inss1 AR-1XA
3 1 2 eqsstri PredRAXA