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 ↾s

Proof

Step	Hyp	Ref	Expression
1		df-ress	⊢ ↾s = ( 𝑤 ∈ V , 𝑎 ∈ V ↦ if ( ( Base ‘ 𝑤 ) ⊆ 𝑎 , 𝑤 , ( 𝑤 sSet ⟨ ( Base ‘ ndx ) , ( 𝑎 ∩ ( Base ‘ 𝑤 ) ) ⟩ ) ) )
2	1	reldmmpo	⊢ Rel dom ↾s