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 ) )