Metamath Proof Explorer

Theorem sucdifsn2

Description: Absorption of union with a singleton by difference. (Contributed by Peter Mazsa, 24-Jul-2024)

Ref Expression
Assertion sucdifsn2 
|- ( ( A u. { A } ) \ { A } ) = A

Proof

Step Hyp Ref Expression
1 disjcsn 
 |-  ( A i^i { A } ) = (/)
2 undif5 
 |-  ( ( A i^i { A } ) = (/) -> ( ( A u. { A } ) \ { A } ) = A )
3 1 2 ax-mp 
 |-  ( ( A u. { A } ) \ { A } ) = A