Theorem relsset

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

	Ref	Expression
Assertion	relsset	⊢ Rel SSet

Proof

Step	Hyp	Ref	Expression
1		df-sset	⊢ SSet = ( ( V × V ) ∖ ran ( E ⊗ ( V ∖ E ) ) )
2		difss	⊢ ( ( V × V ) ∖ ran ( E ⊗ ( V ∖ E ) ) ) ⊆ ( V × V )
3	1 2	eqsstri	⊢ SSet ⊆ ( V × V )
4		df-rel	⊢ ( Rel SSet ↔ SSet ⊆ ( V × V ) )
5	3 4	mpbir	⊢ Rel SSet