Metamath Proof Explorer

Theorem axunprim

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

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

Proof

Step Hyp Ref Expression
1 axunnd 
 |-  E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x )
2 df-an 
 |-  ( ( y e. x /\ x e. z ) <-> -. ( y e. x -> -. x e. z ) )
3 2 exbii 
 |-  ( E. x ( y e. x /\ x e. z ) <-> E. x -. ( y e. x -> -. x e. z ) )
4 exnal 
 |-  ( E. x -. ( y e. x -> -. x e. z ) <-> -. A. x ( y e. x -> -. x e. z ) )
5 3 4 bitri 
 |-  ( E. x ( y e. x /\ x e. z ) <-> -. A. x ( y e. x -> -. x e. z ) )
6 5 imbi1i 
 |-  ( ( E. x ( y e. x /\ x e. z ) -> y e. x ) <-> ( -. A. x ( y e. x -> -. x e. z ) -> y e. x ) )
7 6 albii 
 |-  ( A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) <-> A. y ( -. A. x ( y e. x -> -. x e. z ) -> y e. x ) )
8 7 exbii 
 |-  ( E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) <-> E. x A. y ( -. A. x ( y e. x -> -. x e. z ) -> y e. x ) )
9 df-ex 
 |-  ( E. x A. y ( -. A. x ( y e. x -> -. x e. z ) -> y e. x ) <-> -. A. x -. A. y ( -. A. x ( y e. x -> -. x e. z ) -> y e. x ) )
10 8 9 bitri 
 |-  ( E. x A. y ( E. x ( y e. x /\ x e. z ) -> y e. x ) <-> -. A. x -. A. y ( -. A. x ( y e. x -> -. x e. z ) -> y e. x ) )
11 1 10 mpbi 
 |-  -. A. x -. A. y ( -. A. x ( y e. x -> -. x e. z ) -> y e. x )