Theorem suceqd

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

	Ref	Expression
Hypothesis	suceqd.1	$$⊢\phi \to A=B$$
Assertion	suceqd	$$⊢\phi \to \mathrm{suc}A=\mathrm{suc}B$$

Proof

Step	Hyp	Ref	Expression
1		suceqd.1	$$⊢\phi \to A=B$$
2	1	sneqd	$$⊢\phi \to \left\{A\right\}=\left\{B\right\}$$
3	1 2	uneq12d	$$⊢\phi \to A\cup \left\{A\right\}=B\cup \left\{B\right\}$$
4		df-suc	$$⊢\mathrm{suc}A=A\cup \left\{A\right\}$$
5		df-suc	$$⊢\mathrm{suc}B=B\cup \left\{B\right\}$$
6	3 4 5	3eqtr4g	$$⊢\phi \to \mathrm{suc}A=\mathrm{suc}B$$