Definition df-bj-ccbar 37195

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

Assertion

Ref	Expression
df-bj-ccbar	⊢ ℂ̅ = (ℂ ∪ ℂ∞)

Detailed syntax breakdown of Definition df-bj-ccbar

Step	Hyp	Ref	Expression
1		cccbar 37194	. 2 class ℂ̅
2		cc 11149	. . 3 class ℂ
3		cccinfty 37190	. . 3 class ℂ∞
4	2, 3	cun 3948	. 2 class (ℂ ∪ ℂ∞)
5	1, 4	wceq 1540	1 wff ℂ̅ = (ℂ ∪ ℂ∞)

This definition is referenced by:  bj-ccssccbar  37196  bj-ccinftyssccbar  37197