| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-c | Structured version Visualization version GIF version | ||
| Description: Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 11188. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
| Ref | Expression |
|---|---|
| df-c | ⊢ ℂ = (R × R) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cc 11153 | . 2 class ℂ | |
| 2 | cnr 10905 | . . 3 class R | |
| 3 | 2, 2 | cxp 5683 | . 2 class (R × R) |
| 4 | 1, 3 | wceq 1540 | 1 wff ℂ = (R × R) |
| Colors of variables: wff setvar class |
| This definition is referenced by: opelcn 11169 0ncn 11173 addcnsr 11175 mulcnsr 11176 dfcnqs 11182 axaddf 11185 axmulf 11186 axcnex 11187 axresscn 11188 axcnre 11204 wuncn 11210 bj-inftyexpitaudisj 37206 |
| Copyright terms: Public domain | W3C validator |