Definition df-re 4790

Description: Define a function whose value is the real part of a complex number. See revalt 4794 for its value, recl 4802 for its closure, and replimt 4798 for its use in decomposing a complex number.

Assertion

Ref	Expression
df-re	⊢ ℜ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ∪{z ∈ ℝ∣∃w ∈ ℝ x = (z + (w · i))})}

Distinct variable group(s):   x,y,z,w

Detailed syntax breakdown of Definition df-re

Step	Hyp	Ref	Expression
1		cre 4786	. 2 class ℜ
2		vx	. . . . . 6 set x
3	2	cv 1089	. . . . 5 class x
4		cc 4026	. . . . 5 class ℂ
5	3, 4	wcel 1092	. . . 4 wff x ∈ ℂ
6		vy	. . . . . 6 set y
7	6	cv 1089	. . . . 5 class y
8		vz	. . . . . . . . . . 11 set z
9	8	cv 1089	. . . . . . . . . 10 class z
10		vw	. . . . . . . . . . . 12 set w
11	10	cv 1089	. . . . . . . . . . 11 class w
12		ci 4030	. . . . . . . . . . 11 class i
13		cmulc 4032	. . . . . . . . . . 11 class ·
14	11, 12, 13	co 3001	. . . . . . . . . 10 class (w · i)
15		caddc 4031	. . . . . . . . . 10 class +
16	9, 14, 15	co 3001	. . . . . . . . 9 class (z + (w · i))
17	3, 16	wceq 1091	. . . . . . . 8 wff x = (z + (w · i))
18		cr 4027	. . . . . . . 8 class ℝ
19	17, 10, 18	wrex 1202	. . . . . . 7 wff ∃w ∈ ℝ x = (z + (w · i))
20	19, 8, 18	crab 1204	. . . . . 6 class {z ∈ ℝ∣∃w ∈ ℝ x = (z + (w · i))}
21	20	cuni 1919	. . . . 5 class ∪{z ∈ ℝ∣∃w ∈ ℝ x = (z + (w · i))}
22	7, 21	wceq 1091	. . . 4 wff y = ∪{z ∈ ℝ∣∃w ∈ ℝ x = (z + (w · i))}
23	5, 22	wa 196	. . 3 wff (x ∈ ℂ ∧ y = ∪{z ∈ ℝ∣∃w ∈ ℝ x = (z + (w · i))})
24	23, 2, 6	copab 2055	. 2 class {⟨x, y⟩∣(x ∈ ℂ ∧ y = ∪{z ∈ ℝ∣∃w ∈ ℝ x = (z + (w · i))})}
25	1, 24	wceq 1091	1 wff ℜ = {⟨x, y⟩∣(x ∈ ℂ ∧ y = ∪{z ∈ ℝ∣∃w ∈ ℝ x = (z + (w · i))})}

This definition is referenced by:  revalt 4794

metamath.org