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

Metamath Proof Explorer

Theorem ax12v2-o

Description: Rederivation of ax-c15 from ax12v (without using ax-c15 or the full ax-12 ). Thus, the hypothesis ( ax12v ) provides an alternate axiom that can be used in place of ax-c15 . See also axc15 . (Contributed by NM, 2-Feb-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12v2-o.1 
|- ( x = z -> ( ph -> A. x ( x = z -> ph ) ) )
Assertion ax12v2-o 
|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )

Proof

Step Hyp Ref Expression
1 ax12v2-o.1 
 |-  ( x = z -> ( ph -> A. x ( x = z -> ph ) ) )
2 ax6ev 
 |-  E. z z = y
3 equequ2 
 |-  ( z = y -> ( x = z <-> x = y ) )
4 3 adantl 
 |-  ( ( -. A. x x = y /\ z = y ) -> ( x = z <-> x = y ) )
5 dveeq2-o 
 |-  ( -. A. x x = y -> ( z = y -> A. x z = y ) )
6 5 imp 
 |-  ( ( -. A. x x = y /\ z = y ) -> A. x z = y )
7 nfa1-o 
 |-  F/ x A. x z = y
8 3 imbi1d 
 |-  ( z = y -> ( ( x = z -> ph ) <-> ( x = y -> ph ) ) )
9 8 sps-o 
 |-  ( A. x z = y -> ( ( x = z -> ph ) <-> ( x = y -> ph ) ) )
10 7 9 albid 
 |-  ( A. x z = y -> ( A. x ( x = z -> ph ) <-> A. x ( x = y -> ph ) ) )
11 6 10 syl 
 |-  ( ( -. A. x x = y /\ z = y ) -> ( A. x ( x = z -> ph ) <-> A. x ( x = y -> ph ) ) )
12 11 imbi2d 
 |-  ( ( -. A. x x = y /\ z = y ) -> ( ( ph -> A. x ( x = z -> ph ) ) <-> ( ph -> A. x ( x = y -> ph ) ) ) )
13 4 12 imbi12d 
 |-  ( ( -. A. x x = y /\ z = y ) -> ( ( x = z -> ( ph -> A. x ( x = z -> ph ) ) ) <-> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) )
14 1 13 mpbii 
 |-  ( ( -. A. x x = y /\ z = y ) -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
15 14 ex 
 |-  ( -. A. x x = y -> ( z = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) )
16 15 exlimdv 
 |-  ( -. A. x x = y -> ( E. z z = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) ) )
17 2 16 mpi 
 |-  ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )