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

Metamath Proof Explorer

Theorem relssr

Description: The subset relation is a relation. (Contributed by Peter Mazsa, 1-Aug-2019)

Ref Expression
Assertion relssr Rel S

Proof

Step Hyp Ref Expression
1 df-ssr ⊢ S = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊆ 𝑦 }
2 1 relopabiv ⊢ Rel S