Definition df-we 5614

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 5611	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5609	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5566	. . 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  5634  wess  5645  weeq1  5646  weeq2  5647  wefr  5649  weso  5650  we0  5654  weinxp  5744  wesn  5748  isowe  7354  isowe2  7355  dfwe2  7777  epweon  7778  wexp  8132  wofi  9263  dford5reg  36367  weiunwe  37096  finorwe  38144  fin2so  38369