Definition df-we 5546

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

This definition is referenced by:  nfwe  5565  wess  5576  weeq1  5577  weeq2  5578  wefr  5579  weso  5580  we0  5584  weinxp  5671  wesn  5675  isowe  7220  isowe2  7221  dfwe2  7624  epweon  7625  wexp  7971  wofi  9063  dford5reg  33758  finorwe  35553  fin2so  35764