Description: An element not in a set can be removed without affecting the set. (Contributed by NM, 16-Mar-2006) (Proof shortened by Andrew Salmon, 29-Jun-2011)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | difsn | |- ( -. A e. B -> ( B \ { A } ) = B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eldifsn | |- ( x e. ( B \ { A } ) <-> ( x e. B /\ x =/= A ) ) |
|
| 2 | simpl | |- ( ( x e. B /\ x =/= A ) -> x e. B ) |
|
| 3 | nelelne | |- ( -. A e. B -> ( x e. B -> x =/= A ) ) |
|
| 4 | 3 | ancld | |- ( -. A e. B -> ( x e. B -> ( x e. B /\ x =/= A ) ) ) |
| 5 | 2 4 | impbid2 | |- ( -. A e. B -> ( ( x e. B /\ x =/= A ) <-> x e. B ) ) |
| 6 | 1 5 | bitrid | |- ( -. A e. B -> ( x e. ( B \ { A } ) <-> x e. B ) ) |
| 7 | 6 | eqrdv | |- ( -. A e. B -> ( B \ { A } ) = B ) |