Theorem dfsuccl3

Description: Alternate definition of the class of all successors. (Contributed by Peter Mazsa, 30-Jan-2026)

	Ref	Expression
Assertion	dfsuccl3	Could not format assertion : No typesetting found for |- Suc = { n | E! m suc m = n } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfsuccl2	Could not format Suc = { n | E. m suc m = n } : No typesetting found for |- Suc = { n | E. m suc m = n } with typecode |-
2		exeupre2	$$⊢\exists m\mathrm{suc}m=n\leftrightarrow \exists !m\mathrm{suc}m=n$$
3	2	abbii	$$⊢\left\{n|\exists m\mathrm{suc}m=n\right\}=\left\{n|\exists !m\mathrm{suc}m=n\right\}$$
4	1 3	eqtri	Could not format Suc = { n | E! m suc m = n } : No typesetting found for |- Suc = { n | E! m suc m = n } with typecode |-