Definition df-we 5574

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7713. (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 5571	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5569	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5526	. . 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  5594  wess  5605  weeq1  5606  weeq2  5607  wefr  5609  weso  5610  we0  5614  weinxp  5704  wesn  5708  isowe  7289  isowe2  7290  dfwe2  7713  epweon  7714  wexp  8066  wofi  9179  dford5reg  35831  weiunwe  36520  finorwe  37433  fin2so  37653