Definition df-we 5606

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7763. (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 5603	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5601	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5558	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 395	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 206	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  7338  isowe2  7339  dfwe2  7763  epweon  7764  wexp  8124  wofi  9292  dford5reg  35729  weiunwe  36416  finorwe  37329  fin2so  37560