Theorem relrpss

Description: The proper subset relation is a relation. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Assertion	relrpss	⊢ Rel [⊊]

Proof

Step	Hyp	Ref	Expression
1		df-rpss	⊢ [⊊] = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊊ 𝑦 }
2	1	relopabiv	⊢ Rel [⊊]