Definition df-we 5580

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7721. (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 5577	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5575	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5532	. . 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  5600  wess  5611  weeq1  5612  weeq2  5613  wefr  5615  weso  5616  we0  5620  weinxp  5710  wesn  5714  isowe  7297  isowe2  7298  dfwe2  7721  epweon  7722  wexp  8074  wofi  9193  dford5reg  35955  weiunwe  36644  finorwe  37558  fin2so  37779