Definition df-bj-pinfty

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

	Ref	Expression
Assertion	df-bj-pinfty	$$⊢+\infty =inftyexpi\left(0\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpinfty	$$class+\infty$$
1		cinftyexpi	$$classinftyexpi$$
2		cc0	$$class0$$
3	2 1	cfv	$$classinftyexpi\left(0\right)$$
4	0 3	wceq	$$wff+\infty =inftyexpi\left(0\right)$$