Theorem dfsuccl3

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

	Ref	Expression
Assertion	dfsuccl3	⊢ Suc = { 𝑛 ∣ ∃! 𝑚 suc 𝑚 = 𝑛 }

Proof

Step	Hyp	Ref	Expression
1		dfsuccl2	⊢ Suc = { 𝑛 ∣ ∃ 𝑚 suc 𝑚 = 𝑛 }
2		exeupre2	⊢ ( ∃ 𝑚 suc 𝑚 = 𝑛 ↔ ∃! 𝑚 suc 𝑚 = 𝑛 )
3	2	abbii	⊢ { 𝑛 ∣ ∃ 𝑚 suc 𝑚 = 𝑛 } = { 𝑛 ∣ ∃! 𝑚 suc 𝑚 = 𝑛 }
4	1 3	eqtri	⊢ Suc = { 𝑛 ∣ ∃! 𝑚 suc 𝑚 = 𝑛 }