Metamath Proof Explorer

Theorem axextprim

Description: ax-ext without distinct variable conditions or defined symbols. (Contributed by Scott Fenton, 13-Oct-2010)

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

Proof

Step Hyp Ref Expression
1 axextnd 
 |-  E. x ( ( x e. y <-> x e. z ) -> y = z )
2 dfbi2 
 |-  ( ( x e. y <-> x e. z ) <-> ( ( x e. y -> x e. z ) /\ ( x e. z -> x e. y ) ) )
3 2 imbi1i 
 |-  ( ( ( x e. y <-> x e. z ) -> y = z ) <-> ( ( ( x e. y -> x e. z ) /\ ( x e. z -> x e. y ) ) -> y = z ) )
4 impexp 
 |-  ( ( ( ( x e. y -> x e. z ) /\ ( x e. z -> x e. y ) ) -> y = z ) <-> ( ( x e. y -> x e. z ) -> ( ( x e. z -> x e. y ) -> y = z ) ) )
5 3 4 bitri 
 |-  ( ( ( x e. y <-> x e. z ) -> y = z ) <-> ( ( x e. y -> x e. z ) -> ( ( x e. z -> x e. y ) -> y = z ) ) )
6 5 exbii 
 |-  ( E. x ( ( x e. y <-> x e. z ) -> y = z ) <-> E. x ( ( x e. y -> x e. z ) -> ( ( x e. z -> x e. y ) -> y = z ) ) )
7 df-ex 
 |-  ( E. x ( ( x e. y -> x e. z ) -> ( ( x e. z -> x e. y ) -> y = z ) ) <-> -. A. x -. ( ( x e. y -> x e. z ) -> ( ( x e. z -> x e. y ) -> y = z ) ) )
8 6 7 bitri 
 |-  ( E. x ( ( x e. y <-> x e. z ) -> y = z ) <-> -. A. x -. ( ( x e. y -> x e. z ) -> ( ( x e. z -> x e. y ) -> y = z ) ) )
9 1 8 mpbi 
 |-  -. A. x -. ( ( x e. y -> x e. z ) -> ( ( x e. z -> x e. y ) -> y = z ) )