Theorem brsucmap

Description: Binary relation form of the successor map, general version. (Contributed by Peter Mazsa, 6-Jan-2026)

	Ref	Expression
Assertion	brsucmap	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝑀 SucMap 𝑁 ↔ suc 𝑀 = 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		suceq	⊢ ( 𝑚 = 𝑀 → suc 𝑚 = suc 𝑀 )
2		id	⊢ ( 𝑛 = 𝑁 → 𝑛 = 𝑁 )
3	1 2	eqeqan12d	⊢ ( ( 𝑚 = 𝑀 ∧ 𝑛 = 𝑁 ) → ( suc 𝑚 = 𝑛 ↔ suc 𝑀 = 𝑁 ) )
4		df-sucmap	⊢ SucMap = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
5	3 4	brabga	⊢ ( ( 𝑀 ∈ 𝑉 ∧ 𝑁 ∈ 𝑊 ) → ( 𝑀 SucMap 𝑁 ↔ suc 𝑀 = 𝑁 ) )