This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ R We A \leftrightarrow (R Fr A \land R Or A)$

Step	Hyp	Ref	Expression
0		cR	$class R$
1		cA	$class A$
2	1 0	wwe	$wff R We A$
3	1 0	wfr	$wff R Fr A$
4	1 0	wor	$wff R Or A$
5	3 4	wa	$wff (R Fr A \land R Or A)$
6	2 5	wb	$wff (R We A \leftrightarrow (R Fr A \land R Or A))$