Definition df-rpss 7567

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

Assertion

Ref	Expression
df-rpss	⊢ [⊊] = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-rpss

Step	Hyp	Ref	Expression
1		crpss 7566	. 2 class [⊊]
2		vx	. . . . 5 setvar 𝑥
3	2	cv 1540	. . . 4 class 𝑥
4		vy	. . . . 5 setvar 𝑦
5	4	cv 1540	. . . 4 class 𝑦
6	3, 5	wpss 3892	. . 3 wff 𝑥 ⊊ 𝑦
7	6, 2, 4	copab 5140	. 2 class {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}
8	1, 7	wceq 1541	1 wff [⊊] = {⟨𝑥, 𝑦⟩ ∣ 𝑥 ⊊ 𝑦}

This definition is referenced by:  relrpss  7568  brrpssg  7569