Metamath Proof Explorer

Theorem insucid

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

Ref Expression
Assertion insucid 
|- ( A i^i suc A ) = A

Proof

Step Hyp Ref Expression
1 sssucid 
 |-  A C_ suc A
2 dfss2 
 |-  ( A C_ suc A <-> ( A i^i suc A ) = A )
3 1 2 mpbi 
 |-  ( A i^i suc A ) = A