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 <-> ( R Fr A /\ R Or A ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cR
 |-  R
1 cA
 |-  A
2 1 0 wwe
 |-  R We A
3 1 0 wfr
 |-  R Fr A
4 1 0 wor
 |-  R Or A
5 3 4 wa
 |-  ( R Fr A /\ R Or A )
6 2 5 wb
 |-  ( R We A <-> ( R Fr A /\ R Or A ) )