If \( x \) is not present in \( \varphi \), then \( x \) is not free in \( \varphi \). (Contributed by Mario Carneiro, 11-Aug-2016.) Definition change. (Revised by Wolf Lammen, 12-Sep-2021.)