Theorem suceqsneq

Description: One-to-one relationship between the successor operation and the singleton. (Contributed by Peter Mazsa, 31-Dec-2024)

	Ref	Expression
Assertion	suceqsneq	$$⊢A\in V\to \left(\mathrm{suc}A=\mathrm{suc}B\leftrightarrow \left\{A\right\}=\left\{B\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		suc11reg	$$⊢\mathrm{suc}A=\mathrm{suc}B\leftrightarrow A=B$$
2		sneqbg	$$⊢A\in V\to \left(\left\{A\right\}=\left\{B\right\}\leftrightarrow A=B\right)$$
3	1 2	bitr4id	$$⊢A\in V\to \left(\mathrm{suc}A=\mathrm{suc}B\leftrightarrow \left\{A\right\}=\left\{B\right\}\right)$$