Description: The function value of a mapping M to a restricted binary relation expressed as an ordered-pair class abstraction: The restricted binary relation is a binary relation given as value of a function F restricted by the condition ps . (Contributed by AV, 31-Jan-2021) (Revised by AV, 29-Oct-2021) Add disjoint variable condition on F , x , y to remove a sethood hypothesis. (Revised by SN, 13-Dec-2024)