Metamath Proof Explorer

Theorem preel

Description: Predecessor is a subset of its successor. (Contributed by Peter Mazsa, 12-Jan-2026)

Ref Expression
Assertion preel 
|- ( N e. Suc -> pre N e. N )

Proof

Step Hyp Ref Expression
1 preex 
 |-  pre N e. _V
2 1 sucid 
 |-  pre N e. suc pre N
3 sucpre 
 |-  ( N e. Suc -> suc pre N = N )
4 2 3 eleqtrid 
 |-  ( N e. Suc -> pre N e. N )