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	⊢ [⊊] = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊊ 𝑦 }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crpss	⊢ [⊊]
1		vx	⊢ 𝑥
2		vy	⊢ 𝑦
3	1	cv	⊢ 𝑥
4	2	cv	⊢ 𝑦
5	3 4	wpss	⊢ 𝑥 ⊊ 𝑦
6	5 1 2	copab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊊ 𝑦 }
7	0 6	wceq	⊢ [⊊] = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ⊊ 𝑦 }