Metamath Proof Explorer

Theorem wesn

Description: Well-ordering of a singleton. (Contributed by Mario Carneiro, 28-Dec-2014)

Ref Expression
Assertion wesn 
|- ( Rel R -> ( R We { A } <-> -. A R A ) )

Proof

Step Hyp Ref Expression
1 frsn 
 |-  ( Rel R -> ( R Fr { A } <-> -. A R A ) )
2 sosn 
 |-  ( Rel R -> ( R Or { A } <-> -. A R A ) )
3 1 2 anbi12d 
 |-  ( Rel R -> ( ( R Fr { A } /\ R Or { A } ) <-> ( -. A R A /\ -. A R A ) ) )
4 df-we 
 |-  ( R We { A } <-> ( R Fr { A } /\ R Or { A } ) )
5 pm4.24 
 |-  ( -. A R A <-> ( -. A R A /\ -. A R A ) )
6 3 4 5 3bitr4g 
 |-  ( Rel R -> ( R We { A } <-> -. A R A ) )