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