Definition df-we 5485

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

This definition is referenced by:  nfwe  5501  wess  5512  weeq1  5513  weeq2  5514  wefr  5515  weso  5516  we0  5520  weinxp  5607  wesn  5611  isowe  7115  isowe2  7116  dfwe2  7515  wexp  7850  wofi  8841  dford5reg  33330  finorwe  35176  fin2so  35387