Restricted relation
Set
| context | $X,Y,Z$ |
| context | $R\in \text{Rel}(X,Y)$ |
| postulate | $ \langle x,y\rangle \in R_{|Z}$ |
| postulate | $ \langle x,y\rangle \in R $ |
| postulate | $ x \in Z $ |
Ramifications
Reference
Mizar files: RELAT_1
Wikipedia: Wikipedia: Binary relation