Definition df-we 5633

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7765. (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 395	. 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  5760  wesn  5764  isowe  7349  isowe2  7350  dfwe2  7765  epweon  7766  wexp  8121  wofi  9298  dford5reg  35224  finorwe  36727  fin2so  36939