Theorem axextg

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)

	Ref	Expression
Assertion	axextg	|- ( A. z ( z e. x <-> z e. y ) -> x = y )

Proof

Step	Hyp	Ref	Expression
1		elequ2	|- ( w = x -> ( z e. w <-> z e. x ) )
2	1	bibi1d	|- ( w = x -> ( ( z e. w <-> z e. y ) <-> ( z e. x <-> z e. y ) ) )
3	2	albidv	|- ( w = x -> ( A. z ( z e. w <-> z e. y ) <-> A. z ( z e. x <-> z e. y ) ) )
4		equequ1	|- ( w = x -> ( w = y <-> x = y ) )
5	3 4	imbi12d	|- ( w = x -> ( ( A. z ( z e. w <-> z e. y ) -> w = y ) <-> ( A. z ( z e. x <-> z e. y ) -> x = y ) ) )
6		ax-ext	|- ( A. z ( z e. w <-> z e. y ) -> w = y )
7	5 6	chvarvv	|- ( A. z ( z e. x <-> z e. y ) -> x = y )