Definition df-bj-ccbar

Description: Definition of the set of extended complex numbers CCbar . (Contributed by BJ, 22-Jun-2019)

	Ref	Expression
Assertion	df-bj-ccbar	$$⊢\overline{ℂ}=ℂ\cup {ℂ}_{\infty }$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cccbar	$$class\overline{ℂ}$$
1		cc	$$classℂ$$
2		cccinfty	$$class{ℂ}_{\infty }$$
3	1 2	cun	$$class\left(ℂ\cup {ℂ}_{\infty }\right)$$
4	0 3	wceq	$$wff\overline{ℂ}=ℂ\cup {ℂ}_{\infty }$$