Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eldifd | Unicode version |
Description: If a class is in one class and not another, it is also in their difference. One-way deduction form of eldif 3050. (Contributed by David Moews, 1-May-2017.) |
Ref | Expression |
---|---|
eldifd.1 | |
eldifd.2 |
Ref | Expression |
---|---|
eldifd |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifd.1 | . 2 | |
2 | eldifd.2 | . 2 | |
3 | eldif 3050 | . 2 | |
4 | 1, 2, 3 | sylanbrc 413 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wcel 1465 cdif 3038 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 588 ax-in2 589 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-v 2662 df-dif 3043 |
This theorem is referenced by: exmidundif 4099 exmidundifim 4100 frirrg 4242 dcdifsnid 6368 phpelm 6728 findcard2d 6753 findcard2sd 6754 diffifi 6756 unsnfidcex 6776 unsnfidcel 6777 undifdcss 6779 difinfsnlem 6952 difinfsn 6953 hashunlem 10505 seq3coll 10540 fsum3cvg 11101 isumss 11115 fisumss 11116 |
Copyright terms: Public domain | W3C validator |