Definition df-we 5610

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7812. (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 5607	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5605	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5562	. . 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  5630  wess  5641  weeq1  5642  weeq2  5643  wefr  5645  weso  5646  we0  5650  weinxp  5741  wesn  5745  isowe  7380  isowe2  7381  dfwe2  7812  epweon  7813  wexp  8169  wofi  9308  dford5reg  36722  weiunwe  37435  finorwe  38497  fin2so  38722