Definition df-we 4988

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6850. (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 4985	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 4983	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 4947	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 382	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 194	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5003  wess  5014  weeq1  5015  weeq2  5016  wefr  5017  weso  5018  we0  5022  weinxp  5098  wesn  5102  isowe  6476  isowe2  6477  dfwe2  6850  wexp  7155  wofi  8071  dford5reg  30724  fin2so  32349