Definition df-we 5907

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 5896	. 2 class We
2		cstrict 5894	. . 3 class Or
3		cfound 5895	. . 3 class Fr
4	2, 3	cin 3209	. 2 class ( Or i^i Fr )
5	1, 4	wceq 1642	1 wff We = ( Or i^i Fr )

This definition is referenced by:  weex  5920  weds  5939  nchoicelem8  6297  nchoicelem19  6308