Definition df-cj

Description: Define the complex conjugate function. See cjcli for its closure and cjval for its value. (Contributed by NM, 9-May-1999) (Revised by Mario Carneiro, 6-Nov-2013)

	Ref	Expression
Assertion	df-cj	$$⊢*=\left(x\in ℂ⟼\left(\iota y\in ℂ|\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccj	$$class*$$
1		vx	$$setvarx$$
2		cc	$$classℂ$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		caddc	$$class+$$
6	3	cv	$$setvary$$
7	4 6 5	co	$$class\left(x+y\right)$$
8		cr	$$classℝ$$
9	7 8	wcel	$$wffx+y\in ℝ$$
10		ci	$$class\mathrm{i}$$
11		cmul	$$class\times$$
12		cmin	$$class-$$
13	4 6 12	co	$$class\left(x-y\right)$$
14	10 13 11	co	$$class\mathrm{i}\left(x-y\right)$$
15	14 8	wcel	$$wff\mathrm{i}\left(x-y\right)\in ℝ$$
16	9 15	wa	$$wff\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)$$
17	16 3 2	crio	$$class\left(\iota y\in ℂ|\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)\right)$$
18	1 2 17	cmpt	$$class\left(x\in ℂ⟼\left(\iota y\in ℂ|\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)\right)\right)$$
19	0 18	wceq	$$wff*=\left(x\in ℂ⟼\left(\iota y\in ℂ|\left(x+y\in ℝ\wedge \mathrm{i}\left(x-y\right)\in ℝ\right)\right)\right)$$