Definition df-we 5634

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7775. (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 394	. 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  7354  isowe2  7355  dfwe2  7775  epweon  7776  wexp  8133  wofi  9315  dford5reg  35448  finorwe  36931  fin2so  37150