Definition df-we 5577

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7719. (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 5574	. 2 wff 𝑅 We 𝐴
4	1, 2	wfr 5572	. . 3 wff 𝑅 Fr 𝐴
5	1, 2	wor 5529	. . 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  5597  wess  5608  weeq1  5609  weeq2  5610  wefr  5612  weso  5613  we0  5617  weinxp  5707  wesn  5711  isowe  7295  isowe2  7296  dfwe2  7719  epweon  7720  wexp  8071  wofi  9190  dford5reg  35983  weiunwe  36672  finorwe  37709  fin2so  37939