Theorem omsucelsucb

Description: Membership is inherited by successors for natural numbers. (Contributed by AV, 15-Sep-2023)

	Ref	Expression
Assertion	omsucelsucb	⊢ ( 𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω )

Proof

Step	Hyp	Ref	Expression
1		ordom	⊢ Ord ω
2		ordsucelsuc	⊢ ( Ord ω → ( 𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω ) )
3	1 2	ax-mp	⊢ ( 𝑁 ∈ ω ↔ suc 𝑁 ∈ suc ω )