Theorem relsset

Description: The subset class is a binary relation. (Contributed by Scott Fenton, 31-Mar-2012)

	Ref	Expression
Assertion	relsset	$$⊢\mathrm{Rel}\mathrm{𝖲𝖲𝖾𝗍}$$

Proof

Step	Hyp	Ref	Expression
1		df-sset	$$⊢\mathrm{𝖲𝖲𝖾𝗍}=\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)$$
2		difss	$$⊢\left(\mathrm{V}\times \mathrm{V}\right)\setminus \mathrm{ran}\left(\mathrm{E}\otimes \left(\mathrm{V}\setminus \mathrm{E}\right)\right)\subseteq \mathrm{V}\times \mathrm{V}$$
3	1 2	eqsstri	$$⊢\mathrm{𝖲𝖲𝖾𝗍}\subseteq \mathrm{V}\times \mathrm{V}$$
4		df-rel	$$⊢\mathrm{Rel}\mathrm{𝖲𝖲𝖾𝗍}\leftrightarrow \mathrm{𝖲𝖲𝖾𝗍}\subseteq \mathrm{V}\times \mathrm{V}$$
5	3 4	mpbir	$$⊢\mathrm{Rel}\mathrm{𝖲𝖲𝖾𝗍}$$