Metamath Proof Explorer

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 e. V -> ( suc A = suc B <-> { A } = { B } ) )

Proof

Step Hyp Ref Expression
1 suc11reg 
 |-  ( suc A = suc B <-> A = B )
2 sneqbg 
 |-  ( A e. V -> ( { A } = { B } <-> A = B ) )
3 1 2 bitr4id 
 |-  ( A e. V -> ( suc A = suc B <-> { A } = { B } ) )