Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > difsn | Structured version Visualization version Unicode version |
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 |
---|---|
difsn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifsn 4317 | . . 3 | |
2 | simpl 473 | . . . 4 | |
3 | nelelne 2892 | . . . . 5 | |
4 | 3 | ancld 576 | . . . 4 |
5 | 2, 4 | impbid2 216 | . . 3 |
6 | 1, 5 | syl5bb 272 | . 2 |
7 | 6 | eqrdv 2620 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wa 384 wceq 1483 wcel 1990 wne 2794 cdif 3571 csn 4177 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-v 3202 df-dif 3577 df-sn 4178 |
This theorem is referenced by: difsnb 4337 difsnexi 6970 domdifsn 8043 domunsncan 8060 frfi 8205 infdifsn 8554 dfn2 11305 clslp 20952 xrge00 29686 lindsenlbs 33404 poimirlem2 33411 poimirlem4 33413 poimirlem6 33415 poimirlem7 33416 poimirlem8 33417 poimirlem19 33428 poimirlem23 33432 supxrmnf2 39660 infxrpnf2 39693 dvmptfprodlem 40159 hoiprodp1 40802 |
Copyright terms: Public domain | W3C validator |