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

Metamath Proof Explorer

Theorem relsset

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

		Ref	Expression
	Assertion	relsset	$⊢ Rel 𝖲𝖲𝖾𝗍$

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