Definition df-bj-pinfty 32284

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

Assertion

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

Detailed syntax breakdown of Definition df-bj-pinfty

Step	Hyp	Ref	Expression
1		cpinfty 32283	. 2 class +∞
2		cc0 9815	. . 3 class 0
3		cinftyexpi 32270	. . 3 class inftyexpi
4	2, 3	cfv 5804	. 2 class (inftyexpi ‘0)
5	1, 4	wceq 1475	1 wff +∞ = (inftyexpi ‘0)

This definition is referenced by:  bj-pinftyccb  32285  bj-pinftynrr  32286  bj-pinftynminfty  32291