This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
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 |
⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
snssi |
⊢ ( 𝐵 ∈ 𝐴 → { 𝐵 } ⊆ 𝐴 ) |
| 2 |
|
undifr |
⊢ ( { 𝐵 } ⊆ 𝐴 ↔ ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 ) |
| 3 |
1 2
|
sylib |
⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 ) |