Definition df-we 5616

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7772. (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 5613	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5611	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5568	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 400	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 209	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5636  wess  5647  weeq1  5648  weeq2  5649  wefr  5651  weso  5652  we0  5656  weinxp  5746  wesn  5750  isowe  7347  isowe2  7348  dfwe2  7772  epweon  7773  wexp  8125  wofi  9248  dford5reg  36238  weiunwe  36946  finorwe  37994  fin2so  38224