Definition df-we 5576

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

This definition is referenced by:  nfwe  5596  wess  5607  weeq1  5608  weeq2  5609  wefr  5611  weso  5612  we0  5616  weinxp  5706  wesn  5710  isowe  7297  isowe2  7298  dfwe2  7721  epweon  7722  wexp  8074  wofi  9193  dford5reg  36023  weiunwe  36712  finorwe  37759  fin2so  37989