Definition df-we 5104

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7023. (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 5101	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5099	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5063	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 383	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 196	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5119  wess  5130  weeq1  5131  weeq2  5132  wefr  5133  weso  5134  we0  5138  weinxp  5220  wesn  5224  isowe  6639  isowe2  6640  dfwe2  7023  wexp  7336  wofi  8250  dford5reg  31811  fin2so  33526