This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V , e ∈ V ⟼ s ↾ V ∖ dom ⁡ e ∪ e
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ sSet