Definition df-bj-minfty 37909

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

Assertion

Ref	Expression
df-bj-minfty	⊢ -∞ = (+∞ei‘π)

Detailed syntax breakdown of Definition df-bj-minfty

Step	Hyp	Ref	Expression
1		cminfty 37908	. 2 class -∞
2		cpi 16145	. . 3 class π
3		cinftyexpi 37891	. . 3 class +∞ei
4	2, 3	cfv 6543	. 2 class (+∞ei‘π)
5	1, 4	wceq 1570	1 wff -∞ = (+∞ei‘π)

This definition is used by:  bj-minftyccb  37910  bj-minftynrr  37911  bj-pinftynminfty  37912