Description: No variable is (effectively) free in a non-theorem. (Contributed by Mario Carneiro, 6-Dec-2016) df-nf changed. (Revised by Wolf Lammen, 12-Sep-2021)