Definition df-bj-minfty 33111

Description: Definition of -∞. (Contributed by BJ, 27-Jun-2019.)

Assertion

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

Detailed syntax breakdown of Definition df-bj-minfty

Step	Hyp	Ref	Expression
1		cminfty 33110	. 2 class -∞
2		cpi 14797	. . 3 class π
3		cinftyexpi 33093	. . 3 class inftyexpi
4	2, 3	cfv 5888	. 2 class (inftyexpi ‘π)
5	1, 4	wceq 1483	1 wff -∞ = (inftyexpi ‘π)

This definition is referenced by:  bj-minftyccb  33112  bj-minftynrr  33113  bj-pinftynminfty  33114