Theorem insucid

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

	Ref	Expression
Assertion	insucid	⊢ ( 𝐴 ∩ suc 𝐴 ) = 𝐴

Proof

Step	Hyp	Ref	Expression
1		sssucid	⊢ 𝐴 ⊆ suc 𝐴
2		dfss2	⊢ ( 𝐴 ⊆ suc 𝐴 ↔ ( 𝐴 ∩ suc 𝐴 ) = 𝐴 )
3	1 2	mpbi	⊢ ( 𝐴 ∩ suc 𝐴 ) = 𝐴