Definition df-we 5605

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

This definition is used by:  nfwe  5625  wess  5636  weeq1  5637  weeq2  5638  wefr  5640  weso  5641  we0  5645  weinxp  5735  wesn  5739  isowe  7357  isowe2  7358  dfwe2  7788  epweon  7789  wexp  8144  wofi  9283  dford5reg  36636  weiunwe  37349  finorwe  38398  fin2so  38623