Definition df-we 5634

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7761. (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 5631	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5629	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5588	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 397	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 205	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5653  wess  5664  weeq1  5665  weeq2  5666  wefr  5667  weso  5668  we0  5672  weinxp  5761  wesn  5765  isowe  7346  isowe2  7347  dfwe2  7761  epweon  7762  wexp  8116  wofi  9292  dford5reg  34754  finorwe  36263  fin2so  36475