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=M
Assertion uzssd3 NZNZ

Proof

Step Hyp Ref Expression
1 uzssd3.1 Z=M
2 id NZNZ
3 1 2 uzssd2 NZNZ