Definition df-bj-pinfty 37163

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

Assertion

Ref	Expression
df-bj-pinfty	⊢ +∞ = (+∞ei‘0)

Detailed syntax breakdown of Definition df-bj-pinfty

Step	Hyp	Ref	Expression
1		cpinfty 37162	. 2 class +∞
2		cc0 11146	. . 3 class 0
3		cinftyexpi 37149	. . 3 class +∞ei
4	2, 3	cfv 6558	. 2 class (+∞ei‘0)
5	1, 4	wceq 1535	1 wff +∞ = (+∞ei‘0)

This definition is referenced by:  bj-pinftyccb  37164  bj-pinftynrr  37165  bj-pinftynminfty  37170