Description: A domain has no zero-divisors (besides zero). (Contributed by Jeff Madsen, 19-Jun-2010)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dmnnzd.1 | |
|
dmnnzd.2 | |
||
dmnnzd.3 | |
||
dmnnzd.4 | |
||
Assertion | dmnnzd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmnnzd.1 | |
|
2 | dmnnzd.2 | |
|
3 | dmnnzd.3 | |
|
4 | dmnnzd.4 | |
|
5 | eqid | |
|
6 | 1 2 3 4 5 | isdmn3 | |
7 | 6 | simp3bi | |
8 | oveq1 | |
|
9 | 8 | eqeq1d | |
10 | eqeq1 | |
|
11 | 10 | orbi1d | |
12 | 9 11 | imbi12d | |
13 | oveq2 | |
|
14 | 13 | eqeq1d | |
15 | eqeq1 | |
|
16 | 15 | orbi2d | |
17 | 14 16 | imbi12d | |
18 | 12 17 | rspc2v | |
19 | 7 18 | syl5com | |
20 | 19 | expd | |
21 | 20 | 3imp2 | |