Definition df-we 5536

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7599. (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 5533	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5531	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5492	. . 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  5555  wess  5566  weeq1  5567  weeq2  5568  wefr  5569  weso  5570  we0  5574  weinxp  5661  wesn  5665  isowe  7197  isowe2  7198  dfwe2  7599  wexp  7939  wofi  8968  dford5reg  33639  finorwe  35459  fin2so  35670