Definition df-we 5629

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

This definition is referenced by:  nfwe  5648  wess  5659  weeq1  5660  weeq2  5661  wefr  5662  weso  5663  we0  5667  weinxp  5756  wesn  5760  isowe  7351  isowe2  7352  dfwe2  7770  epweon  7771  wexp  8129  wofi  9308  dford5reg  35314  finorwe  36797  fin2so  37015