Definition df-we

Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 . (Contributed by NM, 3-Apr-1994)

	Ref	Expression
Assertion	df-we	⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	⊢ 𝑅
1		cA	⊢ 𝐴
2	1 0	wwe	⊢ 𝑅 We 𝐴
3	1 0	wfr	⊢ 𝑅 Fr 𝐴
4	1 0	wor	⊢ 𝑅 Or 𝐴
5	3 4	wa	⊢ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 )
6	2 5	wb	⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )