Metamath Proof Explorer

Theorem axpowprim

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

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

Proof

Step Hyp Ref Expression
1 axpownd 
 |-  ( -. x = y -> E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) )
2 df-ex 
 |-  ( E. z x e. y <-> -. A. z -. x e. y )
3 2 imbi1i 
 |-  ( ( E. z x e. y -> A. y x e. z ) <-> ( -. A. z -. x e. y -> A. y x e. z ) )
4 3 albii 
 |-  ( A. x ( E. z x e. y -> A. y x e. z ) <-> A. x ( -. A. z -. x e. y -> A. y x e. z ) )
5 4 imbi1i 
 |-  ( ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) <-> ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) )
6 5 albii 
 |-  ( A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) <-> A. y ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) )
7 6 exbii 
 |-  ( E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) <-> E. x A. y ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) )
8 df-ex 
 |-  ( E. x A. y ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) <-> -. A. x -. A. y ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) )
9 7 8 bitri 
 |-  ( E. x A. y ( A. x ( E. z x e. y -> A. y x e. z ) -> y e. x ) <-> -. A. x -. A. y ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) )
10 1 9 sylib 
 |-  ( -. x = y -> -. A. x -. A. y ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) )
11 10 con4i 
 |-  ( A. x -. A. y ( A. x ( -. A. z -. x e. y -> A. y x e. z ) -> y e. x ) -> x = y )