Definition df-we 5580

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7724. (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 5577	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5575	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5532	. . 3 wff 𝑅 Or 𝐴
6	4, 5	wa 396	. 2 wff (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴)
7	3, 6	wb 207	1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))

This definition is referenced by:  nfwe  5600  wess  5611  weeq1  5612  weeq2  5613  wefr  5615  weso  5616  we0  5620  weinxp  5710  wesn  5714  isowe  7300  isowe2  7301  dfwe2  7724  epweon  7725  wexp  8077  wofi  9196  dford5reg  36009  weiunwe  36698  finorwe  37745  fin2so  37975