Metamath Proof Explorer

Theorem axrepprim

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

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

Proof

Step Hyp Ref Expression
1 axrepnd 
 |-  E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) )
2 df-ex 
 |-  ( E. y A. z ( ph -> z = y ) <-> -. A. y -. A. z ( ph -> z = y ) )
3 df-an 
 |-  ( ( A. z x e. y /\ A. y ph ) <-> -. ( A. z x e. y -> -. A. y ph ) )
4 3 exbii 
 |-  ( E. x ( A. z x e. y /\ A. y ph ) <-> E. x -. ( A. z x e. y -> -. A. y ph ) )
5 exnal 
 |-  ( E. x -. ( A. z x e. y -> -. A. y ph ) <-> -. A. x ( A. z x e. y -> -. A. y ph ) )
6 4 5 bitri 
 |-  ( E. x ( A. z x e. y /\ A. y ph ) <-> -. A. x ( A. z x e. y -> -. A. y ph ) )
7 6 bibi2i 
 |-  ( ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) <-> ( A. y z e. x <-> -. A. x ( A. z x e. y -> -. A. y ph ) ) )
8 dfbi1 
 |-  ( ( A. y z e. x <-> -. A. x ( A. z x e. y -> -. A. y ph ) ) <-> -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) )
9 7 8 bitri 
 |-  ( ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) <-> -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) )
10 9 albii 
 |-  ( A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) <-> A. z -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) )
11 2 10 imbi12i 
 |-  ( ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) <-> ( -. A. y -. A. z ( ph -> z = y ) -> A. z -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) ) )
12 11 exbii 
 |-  ( E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) <-> E. x ( -. A. y -. A. z ( ph -> z = y ) -> A. z -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) ) )
13 df-ex 
 |-  ( E. x ( -. A. y -. A. z ( ph -> z = y ) -> A. z -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) ) <-> -. A. x -. ( -. A. y -. A. z ( ph -> z = y ) -> A. z -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) ) )
14 12 13 bitri 
 |-  ( E. x ( E. y A. z ( ph -> z = y ) -> A. z ( A. y z e. x <-> E. x ( A. z x e. y /\ A. y ph ) ) ) <-> -. A. x -. ( -. A. y -. A. z ( ph -> z = y ) -> A. z -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) ) )
15 1 14 mpbi 
 |-  -. A. x -. ( -. A. y -. A. z ( ph -> z = y ) -> A. z -. ( ( A. y z e. x -> -. A. x ( A. z x e. y -> -. A. y ph ) ) -> -. ( -. A. x ( A. z x e. y -> -. A. y ph ) -> A. y z e. x ) ) )