This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- Pred ( R , A , X ) C_ A

Proof

Step Hyp Ref Expression
1 df-pred 
 |-  Pred ( R , A , X ) = ( A i^i ( `' R " { X } ) )
2 inss1 
 |-  ( A i^i ( `' R " { X } ) ) C_ A
3 1 2 eqsstri 
 |-  Pred ( R , A , X ) C_ A