Theorem reldmsets

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

	Ref	Expression
Assertion	reldmsets	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$$

Proof

Step	Hyp	Ref	Expression
1		df-sets	$$⊢\mathrm{sSet}=\left(s\in \mathrm{V},e\in \mathrm{V}⟼\left({s\upharpoonright }_{\left(\mathrm{V}\setminus \mathrm{dom}\left\{e\right\}\right)}\right)\cup \left\{e\right\}\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{sSet}$$