Definition df-we 5586

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7728. (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 5583	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5581	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5538	. . 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  5606  wess  5617  weeq1  5618  weeq2  5619  wefr  5621  weso  5622  we0  5626  weinxp  5716  wesn  5720  isowe  7304  isowe2  7305  dfwe2  7728  epweon  7729  wexp  8080  wofi  9199  dford5reg  35962  weiunwe  36651  finorwe  37698  fin2so  37928