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

Metamath Proof Explorer

Theorem reldmress

Description: The structure restriction is a proper operator, so it can be used with ovprc1 . (Contributed by Stefan O'Rear, 29-Nov-2014)

		Ref	Expression
	Assertion	reldmress	$⊢ Rel dom ↾_{𝑠}$

Step	Hyp	Ref	Expression
1		df-ress	$⊢ ↾_{𝑠} = (w \in V, a \in V ⟼ if ({Base}_{w} \subseteq a, w, w sSet ⟨{Base}_{ndx}, a \cap {Base}_{w}⟩))$
2	1	reldmmpo	$⊢ Rel dom ↾_{𝑠}$