df-bj-ccinfty - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-ccinfty		Structured version Visualization version Unicode version

Definition df-bj-ccinfty 33099

Description: Definition of the circle at infinity CCinfty. (Contributed by BJ, 22-Jun-2019.) The precise definition is irrelevant and should generally not be used. (New usage is discouraged.)

**Assertion**
Ref	Expression
df-bj-ccinfty	CCinfty inftyexpi

**Detailed syntax breakdown of Definition df-bj-ccinfty**
Step	Hyp	Ref	Expression
1		cccinfty 33098	. 2 CCinfty
2		cinftyexpi 33093	. . 3 inftyexpi
3	2	crn 5115	. 2 inftyexpi
4	1, 3	wceq 1483	1 CCinfty inftyexpi

Colors of variables: wff setvar class

This definition is referenced by: bj-ccinftydisj 33100 bj-elccinfty 33101 bj-minftyccb 33112

W3C validator