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 = ( 𝑠 ∈ V , 𝑒 ∈ V ↦ ( ( 𝑠 ↾ ( V ∖ dom { 𝑒 } ) ) ∪ { 𝑒 } ) )
2	1	reldmmpo	⊢ Rel dom sSet