Definition df-we 5642

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7792. (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 5639	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5637	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5595	. . 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  5663  wess  5674  weeq1  5675  weeq2  5676  wefr  5678  weso  5679  we0  5683  weinxp  5772  wesn  5776  isowe  7368  isowe2  7369  dfwe2  7792  epweon  7793  wexp  8153  wofi  9322  dford5reg  35763  weiunwe  36451  finorwe  37364  fin2so  37593