| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > dtruex | Unicode version | ||
| Description: At least two sets exist
(or in terms of first-order logic, the universe
of discourse has two or more objects). Although dtruarb 4235 can also be
summarized as "at least two sets exist", the difference is
that
dtruarb 4235 shows the existence of two sets which are not
equal to each
other, but this theorem says that given a specific |
| Ref | Expression |
|---|---|
| dtruex |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vex 2775 |
. . . . 5
| |
| 2 | 1 | snex 4229 |
. . . 4
|
| 3 | 2 | isseti 2780 |
. . 3
|
| 4 | elirrv 4596 |
. . . . . . 7
| |
| 5 | vsnid 3665 |
. . . . . . . 8
| |
| 6 | eleq2 2269 |
. . . . . . . 8
| |
| 7 | 5, 6 | mpbiri 168 |
. . . . . . 7
|
| 8 | 4, 7 | mto 664 |
. . . . . 6
|
| 9 | eqtr 2223 |
. . . . . 6
| |
| 10 | 8, 9 | mto 664 |
. . . . 5
|
| 11 | ancom 266 |
. . . . 5
| |
| 12 | 10, 11 | mtbi 672 |
. . . 4
|
| 13 | 12 | imnani 693 |
. . 3
|
| 14 | 3, 13 | eximii 1625 |
. 2
|
| 15 | equcom 1729 |
. . . 4
| |
| 16 | 15 | notbii 670 |
. . 3
|
| 17 | 16 | exbii 1628 |
. 2
|
| 18 | 14, 17 | mpbi 145 |
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-14 2179 ax-ext 2187 ax-sep 4162 ax-pow 4218 ax-setind 4585 |
| This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-nf 1484 df-sb 1786 df-clab 2192 df-cleq 2198 df-clel 2201 df-nfc 2337 df-ne 2377 df-ral 2489 df-v 2774 df-dif 3168 df-in 3172 df-ss 3179 df-pw 3618 df-sn 3639 |
| This theorem is referenced by: dtru 4608 eunex 4609 brprcneu 5569 |
| Copyright terms: Public domain | W3C validator |