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 X. _V ) \ ran ( _E (x) ( _V \ _E ) ) )
2		difss	|- ( ( _V X. _V ) \ ran ( _E (x) ( _V \ _E ) ) ) C_ ( _V X. _V )
3	1 2	eqsstri	|- SSet C_ ( _V X. _V )
4		df-rel	|- ( Rel SSet <-> SSet C_ ( _V X. _V ) )
5	3 4	mpbir	|- Rel SSet