Metamath Proof Explorer


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 )