Definition df-we 5595

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7746. (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 5592	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5590	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5547	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 398	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 208	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5615  wess  5626  weeq1  5627  weeq2  5628  wefr  5630  weso  5631  we0  5635  weinxp  5725  wesn  5729  isowe  7322  isowe2  7323  dfwe2  7746  epweon  7747  wexp  8098  wofi  9222  dford5reg  36078  weiunwe  36777  finorwe  37824  fin2so  38054