Metamath Proof Explorer

Theorem dfdom2

Description: Alternate definition of dominance. (Contributed by NM, 17-Jun-1998)

Ref Expression
Assertion dfdom2 
|- ~<_ = ( ~< u. ~~ )

Proof

Step Hyp Ref Expression
1 df-sdom 
 |-  ~< = ( ~<_ \ ~~ )
2 1 uneq2i 
 |-  ( ~~ u. ~< ) = ( ~~ u. ( ~<_ \ ~~ ) )
3 uncom 
 |-  ( ~~ u. ~< ) = ( ~< u. ~~ )
4 enssdom 
 |-  ~~ C_ ~<_
5 undif 
 |-  ( ~~ C_ ~<_ <-> ( ~~ u. ( ~<_ \ ~~ ) ) = ~<_ )
6 4 5 mpbi 
 |-  ( ~~ u. ( ~<_ \ ~~ ) ) = ~<_
7 2 3 6 3eqtr3ri 
 |-  ~<_ = ( ~< u. ~~ )