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
Parents
Subset of
Binary relation