Description: An element of a set is either equal to another element of the set or a member of the difference of the set and the singleton containing the other element. (Contributed by AV, 25-Aug-2020) (Proof shortened by JJ, 23-Jul-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | eqoreldif | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl | |
|
2 | elsni | |
|
3 | 2 | con3i | |
4 | 3 | adantl | |
5 | 1 4 | eldifd | |
6 | 5 | ex | |
7 | 6 | orrd | |
8 | eleq1a | |
|
9 | eldifi | |
|
10 | 9 | a1i | |
11 | 8 10 | jaod | |
12 | 7 11 | impbid2 | |