Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > eldifbd | Structured version Visualization version Unicode version |
Description: If a class is in the difference of two classes, it is not in the subtrahend. One-way deduction form of eldif 3584. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
eldifbd.1 |
Ref | Expression |
---|---|
eldifbd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifbd.1 | . . 3 | |
2 | eldif 3584 | . . 3 | |
3 | 1, 2 | sylib 208 | . 2 |
4 | 3 | simprd 479 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wa 384 wcel 1990 cdif 3571 |
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-v 3202 df-dif 3577 |
This theorem is referenced by: xpdifid 5562 boxcutc 7951 infeq5i 8533 cantnflem2 8587 ackbij1lem18 9059 infpssrlem4 9128 fin23lem30 9164 domtriomlem 9264 pwfseqlem4 9484 dvdsaddre2b 15029 dprdfadd 18419 pgpfac1lem2 18474 pgpfac1lem3a 18475 pgpfac1lem3 18476 lspsolv 19143 lsppratlem3 19149 mplsubrglem 19439 frlmssuvc2 20134 hauscmplem 21209 1stccnp 21265 1stckgen 21357 alexsublem 21848 bcthlem4 23124 plyeq0lem 23966 ftalem3 24801 tglngne 25445 1loopgrvd0 26400 disjiunel 29409 ofpreima2 29466 qqhval2 30026 esum2dlem 30154 carsgclctunlem1 30379 sibfof 30402 sitgaddlemb 30410 eulerpartlemsv2 30420 eulerpartlemv 30426 eulerpartlemgs2 30442 dochnel2 36681 rmspecnonsq 37472 disjiun2 39226 dstregt0 39493 fprodexp 39826 fprodabs2 39827 fprodcnlem 39831 lptre2pt 39872 dvnprodlem2 40162 stoweidlem43 40260 fourierdlem66 40389 hsphoidmvle2 40799 hsphoidmvle 40800 hoidmvlelem1 40809 hoidmvlelem2 40810 hoidmvlelem3 40811 hoidmvlelem4 40812 |
Copyright terms: Public domain | W3C validator |