Definition df-we 2186

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

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 2062	. 2 wff R We A
4	1, 2	wfr 2061	. . 3 wff R Fr A
5	1, 2	wor 2059	. . 3 wff R Or A
6	4, 5	wa 196	. 2 wff (R Fr A ∧ R Or A)
7	3, 6	wb 127	1 wff (R We A ↔ (R Fr A ∧ R Or A))

This definition is referenced by:  dfwe2 2187  wess 2188  weeq1 2189  weeq2 2190  wefr 2191  weso 2192  we0 2196

metamath.org