Description: Restricted universal quantification ( df-wl-rex ) allows a simplification, if we can assume all occurrences of x in A are bounded. (Contributed by Wolf Lammen, 26-May-2023)