This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem suceqd

Description: Deduction associated with suceq . (Contributed by Rohan Ridenour, 8-Aug-2023)

Ref Expression
Hypothesis suceqd.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
Assertion suceqd ( 𝜑 → suc 𝐴 = suc 𝐵 )

Proof

Step Hyp Ref Expression
1 suceqd.1 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
2 1 sneqd ⊢ ( 𝜑 → { 𝐴 } = { 𝐵 } )
3 1 2 uneq12d ⊢ ( 𝜑 → ( 𝐴 ∪ { 𝐴 } ) = ( 𝐵 ∪ { 𝐵 } ) )
4 df-suc ⊢ suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
5 df-suc ⊢ suc 𝐵 = ( 𝐵 ∪ { 𝐵 } )
6 3 4 5 3eqtr4g ⊢ ( 𝜑 → suc 𝐴 = suc 𝐵 )