Definition df-we 2924

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

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 2906	. 2 wff R We A
4	1, 2	wfr 2905	. . 3 wff R Fr A
5	1, 2	wor 2830	. . 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 2925  wess 2926  weeq1 2927  weeq2 2928  wefr 2929  weso 2930  we0 2934

Copyright terms: Public domain