Description: Substitution applied to an atomic membership wff. (Contributed by Rodolfo Medina, 3-Apr-2010) (Proof shortened by Andrew Salmon, 14-Jun-2011) Reduce axiom usage. (Revised by Wolf Lammen, 24-Jul-2023)