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

Metamath Proof Explorer

Definition df-rpss

Description: Define a relation which corresponds to proper subsethood df-pss on sets. This allows to use proper subsethood with general concepts that require relations, such as strict ordering, see sorpss . (Contributed by Stefan O'Rear, 2-Nov-2014)

		Ref	Expression
	Assertion	df-rpss	$⊢ [\subset] = \{⟨x, y⟩ \| x \subset y\}$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crpss	$class [\subset]$
1		vx	$setvar x$
2		vy	$setvar y$
3	1	cv	$setvar x$
4	2	cv	$setvar y$
5	3 4	wpss	$wff x \subset y$
6	5 1 2	copab	$class \{⟨x, y⟩ \| x \subset y\}$
7	0 6	wceq	$wff [\subset] = \{⟨x, y⟩ \| x \subset y\}$