Description: Ordered pair membership in a restriction when the first member belongs to the restricting class. (Contributed by NM, 30-Apr-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)