Metamath Proof Explorer

Theorem uzssd3

Description: Subset relationship for two sets of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypothesis uzssd3.1 
|- Z = ( ZZ>= ` M )
Assertion uzssd3 
|- ( N e. Z -> ( ZZ>= ` N ) C_ Z )

Proof

Step Hyp Ref Expression
1 uzssd3.1 
 |-  Z = ( ZZ>= ` M )
2 id 
 |-  ( N e. Z -> N e. Z )
3 1 2 uzssd2 
 |-  ( N e. Z -> ( ZZ>= ` N ) C_ Z )