Theorem sucmapsuc

Description: A set is succeeded by its successor. (Contributed by Peter Mazsa, 7-Jan-2026)

	Ref	Expression
Assertion	sucmapsuc	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 SucMap suc 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ suc 𝑀 = suc 𝑀
2		sucexg	⊢ ( 𝑀 ∈ 𝑉 → suc 𝑀 ∈ V )
3		brsucmap	⊢ ( ( 𝑀 ∈ 𝑉 ∧ suc 𝑀 ∈ V ) → ( 𝑀 SucMap suc 𝑀 ↔ suc 𝑀 = suc 𝑀 ) )
4	2 3	mpdan	⊢ ( 𝑀 ∈ 𝑉 → ( 𝑀 SucMap suc 𝑀 ↔ suc 𝑀 = suc 𝑀 ) )
5	1 4	mpbiri	⊢ ( 𝑀 ∈ 𝑉 → 𝑀 SucMap suc 𝑀 )