Metamath Proof Explorer


Theorem uzssd

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

Ref Expression
Hypothesis uzssd.1 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
Assertion uzssd ( 𝜑 → ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) )

Proof

Step Hyp Ref Expression
1 uzssd.1 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
2 uzss ( 𝑁 ∈ ( ℤ𝑀 ) → ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) )
3 1 2 syl ( 𝜑 → ( ℤ𝑁 ) ⊆ ( ℤ𝑀 ) )