Definition df-we 5906

Description: Define the set of all well orderings over a base set. (Contributed by SF, 19-Feb-2015.)

Assertion

Ref	Expression
df-we	|- We = ( Or i^i Fr )

Detailed syntax breakdown of Definition df-we

Step	Hyp	Ref	Expression
1		cwe 5895	. 2 class We
2		cstrict 5893	. . 3 class Or
3		cfound 5894	. . 3 class Fr
4	2, 3	cin 3208	. 2 class ( Or i^i Fr )
5	1, 4	wceq 1642	1 wff We = ( Or i^i Fr )

This definition is referenced by:  weex  5919  weds  5938  nchoicelem8  6294  nchoicelem19  6305