Definition df-we 5593

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7750. (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 5590	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5588	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5545	. . 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  5613  wess  5624  weeq1  5625  weeq2  5626  wefr  5628  weso  5629  we0  5633  weinxp  5723  wesn  5727  isowe  7324  isowe2  7325  dfwe2  7750  epweon  7751  wexp  8109  wofi  9236  dford5reg  35770  weiunwe  36457  finorwe  37370  fin2so  37601