Definition df-bj-minfty

Description: Definition of "minus infinity". (Contributed by BJ, 27-Jun-2019)

	Ref	Expression
Assertion	df-bj-minfty	$$⊢-\infty =inftyexpi\left(\mathrm{\pi }\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cminfty	$$class-\infty$$
1		cinftyexpi	$$classinftyexpi$$
2		cpi	$$class\mathrm{\pi }$$
3	2 1	cfv	$$classinftyexpi\left(\mathrm{\pi }\right)$$
4	0 3	wceq	$$wff-\infty =inftyexpi\left(\mathrm{\pi }\right)$$