df-bj-pinfty - Mathbox for BJ

	Mathbox for BJ		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df-bj-pinfty		Structured version Visualization version GIF version

Definition df-bj-pinfty 33107

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 33106	. 2 class +∞
2		cc0 9936	. . 3 class 0
3		cinftyexpi 33093	. . 3 class inftyexpi
4	2, 3	cfv 5888	. 2 class (inftyexpi ‘0)
5	1, 4	wceq 1483	1 wff +∞ = (inftyexpi ‘0)

Colors of variables: wff setvar class

This definition is referenced by: bj-pinftyccb 33108 bj-pinftynrr 33109 bj-pinftynminfty 33114