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	⊢ ℂ̅ = ( ℂ ∪ ℂ∞ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cccbar	⊢ ℂ̅
1		cc	⊢ ℂ
2		cccinfty	⊢ ℂ∞
3	1 2	cun	⊢ ( ℂ ∪ ℂ∞ )
4	0 3	wceq	⊢ ℂ̅ = ( ℂ ∪ ℂ∞ )