Definition df-we 5606

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7777. (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 401	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 209	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is used by:  nfwe  5626  wess  5637  weeq1  5638  weeq2  5639  wefr  5641  weso  5642  we0  5646  weinxp  5736  wesn  5740  isowe  7349  isowe2  7350  dfwe2  7777  epweon  7778  wexp  8131  wofi  9264  dford5reg  36511  weiunwe  37224  finorwe  38270  fin2so  38495