This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem difsnid

Description: If we remove a single element from a class then put it back in, we end up with the original class. (Contributed by NM, 2-Oct-2006)

Ref Expression
Assertion difsnid ⊢ B ∈ A → A ∖ B ∪ B = A

Proof

Step Hyp Ref Expression
1 snssi ⊢ B ∈ A → B ⊆ A
2 undifr ⊢ B ⊆ A ↔ A ∖ B ∪ B = A
3 1 2 sylib ⊢ B ∈ A → A ∖ B ∪ B = A