Description: A variable introduction law for equality. Lemma 15 of Monk2 p. 109,
however we do not require z to be distinct from x and y .
Usage of this theorem is discouraged because it depends on ax-13 . See
equvinv for a shorter proof requiring fewer axioms when z is
required to be distinct from x and y . (Contributed by NM, 10-Jan-1993)(Proof shortened by Andrew Salmon, 25-May-2011)(Proof
shortened by Wolf Lammen, 16-Sep-2023)(New usage is discouraged.)