Theorem brsucmap

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

	Ref	Expression
Assertion	brsucmap	Could not format assertion : No typesetting found for |- ( ( M e. V /\ N e. W ) -> ( M SucMap N <-> suc M = N ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		suceq	$$⊢m=M\to \mathrm{suc}m=\mathrm{suc}M$$
2		id	$$⊢n=N\to n=N$$
3	1 2	eqeqan12d	$$⊢\left(m=M\wedge n=N\right)\to \left(\mathrm{suc}m=n\leftrightarrow \mathrm{suc}M=N\right)$$
4		df-sucmap	Could not format SucMap = { <. m , n >. | suc m = n } : No typesetting found for |- SucMap = { <. m , n >. | suc m = n } with typecode |-
5	3 4	brabga	Could not format ( ( M e. V /\ N e. W ) -> ( M SucMap N <-> suc M = N ) ) : No typesetting found for |- ( ( M e. V /\ N e. W ) -> ( M SucMap N <-> suc M = N ) ) with typecode |-