Definition df-we 5621

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7782. (Contributed by NM, 3-Apr-1994.)

Assertion

Ref	Expression
df-we	⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

Detailed syntax breakdown of Definition df-we

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3	1, 2	wwe 5618	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5616	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5573	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 401	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 209	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is used by:  nfwe  5641  wess  5652  weeq1  5653  weeq2  5654  wefr  5656  weso  5657  we0  5661  weinxp  5751  wesn  5755  isowe  7358  isowe2  7359  dfwe2  7782  epweon  7783  wexp  8135  wofi  9259  dford5reg  36285  weiunwe  37013  finorwe  38061  fin2so  38291