Theorem ax12inda

Description: Induction step for constructing a substitution instance of ax-c15 without using ax-c15 . Quantification case. (When z and y are distinct, ax12inda2 may be used instead to avoid the dummy variable w in the proof.) (Contributed by NM, 24-Jan-2007) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax12inda.1	|- ( -. A. x x = w -> ( x = w -> ( ph -> A. x ( x = w -> ph ) ) ) )
2		ax6ev	|- E. w w = y
3	1	ax12inda2	|- ( -. A. x x = w -> ( x = w -> ( A. z ph -> A. x ( x = w -> A. z ph ) ) ) )
4		dveeq2-o	|- ( -. A. x x = y -> ( w = y -> A. x w = y ) )
5	4	imp	|- ( ( -. A. x x = y /\ w = y ) -> A. x w = y )
6		hba1-o	|- ( A. x w = y -> A. x A. x w = y )
7		equequ2	|- ( w = y -> ( x = w <-> x = y ) )
8	7	sps-o	|- ( A. x w = y -> ( x = w <-> x = y ) )
9	6 8	albidh	|- ( A. x w = y -> ( A. x x = w <-> A. x x = y ) )
10	9	notbid	|- ( A. x w = y -> ( -. A. x x = w <-> -. A. x x = y ) )
11	5 10	syl	|- ( ( -. A. x x = y /\ w = y ) -> ( -. A. x x = w <-> -. A. x x = y ) )
12	7	adantl	|- ( ( -. A. x x = y /\ w = y ) -> ( x = w <-> x = y ) )
13	8	imbi1d	|- ( A. x w = y -> ( ( x = w -> A. z ph ) <-> ( x = y -> A. z ph ) ) )
14	6 13	albidh	|- ( A. x w = y -> ( A. x ( x = w -> A. z ph ) <-> A. x ( x = y -> A. z ph ) ) )
15	5 14	syl	|- ( ( -. A. x x = y /\ w = y ) -> ( A. x ( x = w -> A. z ph ) <-> A. x ( x = y -> A. z ph ) ) )
16	15	imbi2d	|- ( ( -. A. x x = y /\ w = y ) -> ( ( A. z ph -> A. x ( x = w -> A. z ph ) ) <-> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
17	12 16	imbi12d	|- ( ( -. A. x x = y /\ w = y ) -> ( ( x = w -> ( A. z ph -> A. x ( x = w -> A. z ph ) ) ) <-> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
18	11 17	imbi12d	|- ( ( -. A. x x = y /\ w = y ) -> ( ( -. A. x x = w -> ( x = w -> ( A. z ph -> A. x ( x = w -> A. z ph ) ) ) ) <-> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) ) )
19	3 18	mpbii	|- ( ( -. A. x x = y /\ w = y ) -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
20	19	ex	|- ( -. A. x x = y -> ( w = y -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) ) )
21	20	exlimdv	|- ( -. A. x x = y -> ( E. w w = y -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) ) )
22	2 21	mpi	|- ( -. A. x x = y -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
23	22	pm2.43i	|- ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )