Metamath Proof Explorer

Theorem pred0

Description: The predecessor class over (/) is always (/) . (Contributed by Scott Fenton, 16-Apr-2011) (Proof shortened by AV, 11-Jun-2021)

Ref Expression
Assertion pred0 
|- Pred ( R , (/) , X ) = (/)

Proof

Step Hyp Ref Expression
1 df-pred 
 |-  Pred ( R , (/) , X ) = ( (/) i^i ( `' R " { X } ) )
2 0in 
 |-  ( (/) i^i ( `' R " { X } ) ) = (/)
3 1 2 eqtri 
 |-  Pred ( R , (/) , X ) = (/)