Theorem we0

Description: Any relation is a well-ordering of the empty set. (Contributed by NM, 16-Mar-1997)

	Ref	Expression
Assertion	we0	⊢ 𝑅 We ∅

Proof

Step	Hyp	Ref	Expression
1		fr0	⊢ 𝑅 Fr ∅
2		so0	⊢ 𝑅 Or ∅
3		df-we	⊢ ( 𝑅 We ∅ ↔ ( 𝑅 Fr ∅ ∧ 𝑅 Or ∅ ) )
4	1 2 3	mpbir2an	⊢ 𝑅 We ∅