Description: Substitution applied to an atomic membership wff. (Contributed by NM, 7-Nov-2006) (Proof shortened by Andrew Salmon, 14-Jun-2011) Reduce axiom usage. (Revised by Wolf Lammen, 24-Jul-2023)