Definition df-we 2929

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

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 2911	. 2 wff R We A
4	1, 2	wfr 2910	. . 3 wff R Fr A
5	1, 2	wor 2834	. . 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 2930  wess 2931  weeq1 2932  weeq2 2933  wefr 2934  weso 2935  we0 2939

Copyright terms: Public domain