Description: Alternate definition of dominance. (Contributed by NM, 17-Jun-1998)
Ref | Expression | ||
---|---|---|---|
Assertion | dfdom2 | |- ~<_ = ( ~< u. ~~ ) |
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. ~~ ) |