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 ) ) ) )