This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )