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 Reldom𝑠

Proof

Step Hyp Ref Expression
1 df-ress 𝑠=wV,aVifBasewawwsSetBasendxaBasew
2 1 reldmmpo Reldom𝑠