Metamath Proof Explorer

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 
|- CCbar = ( CC u. CCinfty )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cccbar 
 |-  CCbar
1 cc 
 |-  CC
2 cccinfty 
 |-  CCinfty
3 1 2 cun 
 |-  ( CC u. CCinfty )
4 0 3 wceq 
 |-  CCbar = ( CC u. CCinfty )