Definition df-we 5654

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7809. (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 5651	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5649	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5606	. . 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  5675  wess  5686  weeq1  5687  weeq2  5688  wefr  5690  weso  5691  we0  5695  weinxp  5784  wesn  5788  isowe  7385  isowe2  7386  dfwe2  7809  epweon  7810  wexp  8171  wofi  9353  dford5reg  35746  weiunwe  36435  finorwe  37348  fin2so  37567