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 |
|