Definition df-we 2934

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

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 2916	. 2 wff R We A
4	1, 2	wfr 2915	. . 3 wff R Fr A
5	1, 2	wor 2839	. . 3 wff R Or A
6	4, 5	wa 223	. 2 wff (R Fr A /\ R Or A)
7	3, 6	wb 146	1 wff (R We A <-> (R Fr A /\ R Or A))

This definition is referenced by:  dfwe2 2935  wess 2936  weeq1 2937  weeq2 2938  wefr 2939  weso 2940  we0 2944

Copyright terms: Public domain