| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > disj | Unicode version | ||
| Description: Two ways of saying that two classes are disjoint (have no members in common). (Contributed by NM, 17-Feb-2004.) |
| Ref | Expression |
|---|---|
| disj |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-in 3172 |
. . . 4
| |
| 2 | 1 | eqeq1i 2213 |
. . 3
|
| 3 | abeq1 2315 |
. . 3
| |
| 4 | imnan 692 |
. . . . 5
| |
| 5 | noel 3464 |
. . . . . 6
| |
| 6 | 5 | nbn 701 |
. . . . 5
|
| 7 | 4, 6 | bitr2i 185 |
. . . 4
|
| 8 | 7 | albii 1493 |
. . 3
|
| 9 | 2, 3, 8 | 3bitri 206 |
. 2
|
| 10 | df-ral 2489 |
. 2
| |
| 11 | 9, 10 | bitr4i 187 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1470 ax-7 1471 ax-gen 1472 ax-ie1 1516 ax-ie2 1517 ax-8 1527 ax-10 1528 ax-11 1529 ax-i12 1530 ax-bndl 1532 ax-4 1533 ax-17 1549 ax-i9 1553 ax-ial 1557 ax-i5r 1558 ax-ext 2187 |
| This theorem depends on definitions: df-bi 117 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ral 2489 df-v 2774 df-dif 3168 df-in 3172 df-nul 3461 |
| This theorem is referenced by: disjr 3510 disj1 3511 disjne 3514 f0rn0 5470 renfdisj 8132 fvinim0ffz 10370 xnn0nnen 10582 fxnn0nninf 10584 fprodsplitdc 11907 exmidunben 12797 dedekindeulemuub 15089 dedekindeulemlu 15093 dedekindicclemuub 15098 dedekindicclemlu 15102 ivthinclemdisj 15112 exmidsbthrlem 15961 |
| Copyright terms: Public domain | W3C validator |