Definition df-we 5569

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7702. (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 5566	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5564	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5521	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 395	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 206	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5589  wess  5600  weeq1  5601  weeq2  5602  wefr  5604  weso  5605  we0  5609  weinxp  5699  wesn  5703  isowe  7278  isowe2  7279  dfwe2  7702  epweon  7703  wexp  8055  wofi  9168  dford5reg  35795  weiunwe  36482  finorwe  37395  fin2so  37626