Definition df-we 5516

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7496. (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 5513	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5511	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5473	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 398	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 208	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5531  wess  5542  weeq1  5543  weeq2  5544  wefr  5545  weso  5546  we0  5550  weinxp  5636  wesn  5640  isowe  7102  isowe2  7103  dfwe2  7496  wexp  7824  wofi  8767  dford5reg  33027  finorwe  34666  fin2so  34894