Metamath Proof Explorer


Theorem bj-ccssccbar

Description: Complex numbers are extended complex numbers. (Contributed by BJ, 27-Jun-2019)

Ref Expression
Assertion bj-ccssccbar ℂ ⊆ ℂ̅

Proof

Step Hyp Ref Expression
1 ssun1 ℂ ⊆ ( ℂ ∪ ℂ )
2 df-bj-ccbar ℂ̅ = ( ℂ ∪ ℂ )
3 1 2 sseqtrri ℂ ⊆ ℂ̅