Definition df-we 2962

Description: Define a well-ordering. For an alternate definition, see dfwe2 3140.

Assertion

Ref	Expression
df-we	|- (R We A <-> (R Fr A /\ R Or A))

Detailed syntax breakdown of Definition df-we

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wwe 2946	. 2 wff R We A
4	1, 2	wfr 2945	. . 3 wff R Fr A
5	1, 2	wor 2917	. . 3 wff R Or A
6	4, 5	wa 221	. 2 wff (R Fr A /\ R Or A)
7	3, 6	wb 144	1 wff (R We A <-> (R Fr A /\ R Or A))

This definition is referenced by:  wess 2963  weeq1 2964  weeq2 2965  wefr 2966  weso 2967  we0 2971  dfwe2 3140

Copyright terms: Public domain