Definition df-we 5578

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7714. (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 5575	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5573	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5530	. . 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  5598  wess  5609  weeq1  5610  weeq2  5611  wefr  5613  weso  5614  we0  5618  weinxp  5708  wesn  5712  isowe  7290  isowe2  7291  dfwe2  7714  epweon  7715  wexp  8070  wofi  9194  dford5reg  35755  weiunwe  36442  finorwe  37355  fin2so  37586