Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | bnj1143 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iun | |
|
2 | notnotb | |
|
3 | neq0 | |
|
4 | 2 3 | xchbinx | |
5 | df-rex | |
|
6 | exsimpl | |
|
7 | 5 6 | sylbi | |
8 | 7 | con3i | |
9 | 4 8 | sylbi | |
10 | 9 | alrimiv | |
11 | notnotb | |
|
12 | neq0 | |
|
13 | 1 | eqeq1i | |
14 | 13 | notbii | |
15 | df-iun | |
|
16 | 15 | eleq2i | |
17 | 16 | exbii | |
18 | 12 14 17 | 3bitr3i | |
19 | 11 18 | xchbinx | |
20 | alnex | |
|
21 | abid | |
|
22 | 21 | notbii | |
23 | 22 | albii | |
24 | 19 20 23 | 3bitr2i | |
25 | 10 24 | sylibr | |
26 | 1 25 | eqtrid | |
27 | 0ss | |
|
28 | 26 27 | eqsstrdi | |
29 | iunconst | |
|
30 | eqimss | |
|
31 | 29 30 | syl | |
32 | 28 31 | pm2.61ine | |