Definition df-we 5480

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

This definition is referenced by:  nfwe  5495  wess  5506  weeq1  5507  weeq2  5508  wefr  5509  weso  5510  we0  5514  weinxp  5600  wesn  5604  isowe  7081  isowe2  7082  dfwe2  7476  wexp  7807  wofi  8751  dford5reg  33140  finorwe  34799  fin2so  35044