Definition df-we 5607

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 5604	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5602	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5559	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 400	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 209	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5627  wess  5638  weeq1  5639  weeq2  5640  wefr  5642  weso  5643  we0  5647  weinxp  5737  wesn  5741  isowe  7337  isowe2  7338  dfwe2  7761  epweon  7762  wexp  8114  wofi  9237  dford5reg  36143  weiunwe  36842  finorwe  37888  fin2so  38118