Theorem insucid

Description: The intersection of a class and its successor is itself. (Contributed by RP, 3-Jan-2025)

	Ref	Expression
Assertion	insucid	$$⊢A\cap \mathrm{suc}A=A$$

Proof

Step	Hyp	Ref	Expression
1		sssucid	$$⊢A\subseteq \mathrm{suc}A$$
2		dfss2	$$⊢A\subseteq \mathrm{suc}A\leftrightarrow A\cap \mathrm{suc}A=A$$
3	1 2	mpbi	$$⊢A\cap \mathrm{suc}A=A$$