Metamath Proof Explorer

Theorem reldmsets

Description: The structure override operator is a proper operator. (Contributed by Stefan O'Rear, 29-Jan-2015)

Ref Expression
Assertion reldmsets 
|- Rel dom sSet

Proof

Step Hyp Ref Expression
1 df-sets 
 |-  sSet = ( s e. _V , e e. _V |-> ( ( s |` ( _V \ dom { e } ) ) u. { e } ) )
2 1 reldmmpo 
 |-  Rel dom sSet