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\mathrm{We}A\leftrightarrow \left(R\mathrm{Fr}A\wedge R\mathrm{Or}A\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cR	$$classR$$
1		cA	$$classA$$
2	1 0	wwe	$$wffR\mathrm{We}A$$
3	1 0	wfr	$$wffR\mathrm{Fr}A$$
4	1 0	wor	$$wffR\mathrm{Or}A$$
5	3 4	wa	$$wff\left(R\mathrm{Fr}A\wedge R\mathrm{Or}A\right)$$
6	2 5	wb	$$wff\left(R\mathrm{We}A\leftrightarrow \left(R\mathrm{Fr}A\wedge R\mathrm{Or}A\right)\right)$$