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	⊢ ( 𝐴 ∈ 𝑉 → ( suc 𝐴 = suc 𝐵 ↔ { 𝐴 } = { 𝐵 } ) )

Proof

Step	Hyp	Ref	Expression
1		suc11reg	⊢ ( suc 𝐴 = suc 𝐵 ↔ 𝐴 = 𝐵 )
2		sneqbg	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐵 } ↔ 𝐴 = 𝐵 ) )
3	1 2	bitr4id	⊢ ( 𝐴 ∈ 𝑉 → ( suc 𝐴 = suc 𝐵 ↔ { 𝐴 } = { 𝐵 } ) )