Description: Two ways of expressing " x is (effectively) not free in ph ". (Contributed by Gérard Lang, 14-Nov-2013) (Revised by Mario Carneiro, 6-Oct-2016) (Proof shortened by Wolf Lammen, 22-Sep-2018) Avoid ax-13 . (Revised by Wolf Lammen, 30-Jan-2023)