Definition df-we 5639

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7794. (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 5636	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5634	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5591	. . 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  5660  wess  5671  weeq1  5672  weeq2  5673  wefr  5675  weso  5676  we0  5680  weinxp  5770  wesn  5774  isowe  7369  isowe2  7370  dfwe2  7794  epweon  7795  wexp  8155  wofi  9325  dford5reg  35783  weiunwe  36470  finorwe  37383  fin2so  37614