Definition df-we 5633

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7758. (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 5630	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5628	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5587	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 397	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 205	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5652  wess  5663  weeq1  5664  weeq2  5665  wefr  5666  weso  5667  we0  5671  weinxp  5759  wesn  5763  isowe  7343  isowe2  7344  dfwe2  7758  epweon  7759  wexp  8113  wofi  9289  dford5reg  34743  finorwe  36252  fin2so  36464