Definition df-we 5587

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7729. (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 5584	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5582	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5539	. . 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  5607  wess  5618  weeq1  5619  weeq2  5620  wefr  5622  weso  5623  we0  5627  weinxp  5717  wesn  5721  isowe  7305  isowe2  7306  dfwe2  7729  epweon  7730  wexp  8082  wofi  9201  dford5reg  35993  weiunwe  36682  finorwe  37626  fin2so  37847