Description: A generalization of the axiom of extensionality in which x and y
need not be distinct. (Contributed by NM, 15-Sep-1993)(Proof
shortened by Andrew Salmon, 12-Aug-2011) Remove dependencies on
ax-10 , ax-12 , ax-13 . (Revised by BJ, 12-Jul-2019)(Revised by Wolf Lammen, 9-Dec-2019)