Definition df-we 5045

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6943. (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 5042	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5040	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5004	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 384	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 196	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5060  wess  5071  weeq1  5072  weeq2  5073  wefr  5074  weso  5075  we0  5079  weinxp  5157  wesn  5161  isowe  6564  isowe2  6565  dfwe2  6943  wexp  7251  wofi  8169  dford5reg  31441  fin2so  33067