Definition df-we 5608

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7766. (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 5605	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5603	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5560	. . 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  5629  wess  5640  weeq1  5641  weeq2  5642  wefr  5644  weso  5645  we0  5649  weinxp  5739  wesn  5743  isowe  7341  isowe2  7342  dfwe2  7766  epweon  7767  wexp  8127  wofi  9295  dford5reg  35746  weiunwe  36433  finorwe  37346  fin2so  37577