This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-e

Description: Define Euler's constant _e = 2.71828.... (Contributed by NM, 14-Mar-2005)

		Ref	Expression
	Assertion	df-e	$⊢ e = e^{1}$

Step	Hyp	Ref	Expression
0		ceu	$class e$
1		ce	$class \exp$
2		c1	$class 1$
3	2 1	cfv	$class e^{1}$
4	0 3	wceq	$wff e = e^{1}$