Definition df-we 5596

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7753. (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 5593	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5591	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5548	. . 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  5616  wess  5627  weeq1  5628  weeq2  5629  wefr  5631  weso  5632  we0  5636  weinxp  5726  wesn  5730  isowe  7327  isowe2  7328  dfwe2  7753  epweon  7754  wexp  8112  wofi  9243  dford5reg  35777  weiunwe  36464  finorwe  37377  fin2so  37608