Theorem ax12eq 32576

Description: Basis step for constructing a substitution instance of ax-c15 32525 without using ax-c15 32525. Atomic formula for equality predicate. (Contributed by NM, 22-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ax12eq	|- ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )

Proof of Theorem ax12eq

Dummy variables u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		19.26 1740	. . 3 |- ( A. x ( x = z /\ x = w ) <-> ( A. x x = z /\ A. x x = w ) )
2		equid 1863	. . . . . . . 8 |- x = x
3	2	a1i 11	. . . . . . 7 |- ( x = y -> x = x )
4	3	ax-gen 1677	. . . . . 6 |- A. x ( x = y -> x = x )
5	4	a1i 11	. . . . 5 |- ( x = x -> A. x ( x = y -> x = x ) )
6		equequ1 1875	. . . . . . . . 9 |- ( x = z -> ( x = x <-> z = x ) )
7		equequ2 1876	. . . . . . . . 9 |- ( x = w -> ( z = x <-> z = w ) )
8	6, 7	sylan9bb 714	. . . . . . . 8 |- ( ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
9	8	sps-o 32543	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
10		nfa1-o 32550	. . . . . . . 8 |- F/ x A. x ( x = z /\ x = w )
11	9	imbi2d 323	. . . . . . . 8 |- ( A. x ( x = z /\ x = w ) -> ( ( x = y -> x = x ) <-> ( x = y -> z = w ) ) )
12	10, 11	albid 1983	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( A. x ( x = y -> x = x ) <-> A. x ( x = y -> z = w ) ) )
13	9, 12	imbi12d 327	. . . . . 6 |- ( A. x ( x = z /\ x = w ) -> ( ( x = x -> A. x ( x = y -> x = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
14	13	adantr 472	. . . . 5 |- ( ( A. x ( x = z /\ x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( ( x = x -> A. x ( x = y -> x = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
15	5, 14	mpbii 216	. . . 4 |- ( ( A. x ( x = z /\ x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
16	15	exp32 616	. . 3 |- ( A. x ( x = z /\ x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
17	1, 16	sylbir 218	. 2 |- ( ( A. x x = z /\ A. x x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
18		equequ1 1875	. . . . . . 7 |- ( x = y -> ( x = w <-> y = w ) )
19	18	ad2antll 743	. . . . . 6 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w <-> y = w ) )
20		axc9 2154	. . . . . . . . 9 |- ( -. A. x x = y -> ( -. A. x x = w -> ( y = w -> A. x y = w ) ) )
21	20	impcom 437	. . . . . . . 8 |- ( ( -. A. x x = w /\ -. A. x x = y ) -> ( y = w -> A. x y = w ) )
22	21	adantrr 731	. . . . . . 7 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x y = w ) )
23		equtrr 1874	. . . . . . . 8 |- ( y = w -> ( x = y -> x = w ) )
24	23	alimi 1692	. . . . . . 7 |- ( A. x y = w -> A. x ( x = y -> x = w ) )
25	22, 24	syl6 33	. . . . . 6 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x ( x = y -> x = w ) ) )
26	19, 25	sylbid 223	. . . . 5 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w -> A. x ( x = y -> x = w ) ) )
27	26	adantll 728	. . . 4 |- ( ( ( A. x x = z /\ -. A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w -> A. x ( x = y -> x = w ) ) )
28		equequ1 1875	. . . . . . 7 |- ( x = z -> ( x = w <-> z = w ) )
29	28	sps-o 32543	. . . . . 6 |- ( A. x x = z -> ( x = w <-> z = w ) )
30	29	imbi2d 323	. . . . . . 7 |- ( A. x x = z -> ( ( x = y -> x = w ) <-> ( x = y -> z = w ) ) )
31	30	dral2-o 32565	. . . . . 6 |- ( A. x x = z -> ( A. x ( x = y -> x = w ) <-> A. x ( x = y -> z = w ) ) )
32	29, 31	imbi12d 327	. . . . 5 |- ( A. x x = z -> ( ( x = w -> A. x ( x = y -> x = w ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
33	32	ad2antrr 740	. . . 4 |- ( ( ( A. x x = z /\ -. A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( ( x = w -> A. x ( x = y -> x = w ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
34	27, 33	mpbid 215	. . 3 |- ( ( ( A. x x = z /\ -. A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
35	34	exp32 616	. 2 |- ( ( A. x x = z /\ -. A. x x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
36		equequ2 1876	. . . . . . 7 |- ( x = y -> ( z = x <-> z = y ) )
37	36	ad2antll 743	. . . . . 6 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x <-> z = y ) )
38		axc9 2154	. . . . . . . . 9 |- ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
39	38	imp 436	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
40	39	adantrr 731	. . . . . . 7 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x z = y ) )
41	36	biimprcd 233	. . . . . . . 8 |- ( z = y -> ( x = y -> z = x ) )
42	41	alimi 1692	. . . . . . 7 |- ( A. x z = y -> A. x ( x = y -> z = x ) )
43	40, 42	syl6 33	. . . . . 6 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x ( x = y -> z = x ) ) )
44	37, 43	sylbid 223	. . . . 5 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x -> A. x ( x = y -> z = x ) ) )
45	44	adantlr 729	. . . 4 |- ( ( ( -. A. x x = z /\ A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x -> A. x ( x = y -> z = x ) ) )
46	7	sps-o 32543	. . . . . 6 |- ( A. x x = w -> ( z = x <-> z = w ) )
47	46	imbi2d 323	. . . . . . 7 |- ( A. x x = w -> ( ( x = y -> z = x ) <-> ( x = y -> z = w ) ) )
48	47	dral2-o 32565	. . . . . 6 |- ( A. x x = w -> ( A. x ( x = y -> z = x ) <-> A. x ( x = y -> z = w ) ) )
49	46, 48	imbi12d 327	. . . . 5 |- ( A. x x = w -> ( ( z = x -> A. x ( x = y -> z = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
50	49	ad2antlr 741	. . . 4 |- ( ( ( -. A. x x = z /\ A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( ( z = x -> A. x ( x = y -> z = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
51	45, 50	mpbid 215	. . 3 |- ( ( ( -. A. x x = z /\ A. x x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
52	51	exp32 616	. 2 |- ( ( -. A. x x = z /\ A. x x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
53		ax6ev 1815	. . . . 5 |- E. u u = w
54		ax6ev 1815	. . . . . . 7 |- E. v v = z
55		ax-1 6	. . . . . . . . . . 11 |- ( v = u -> ( x = y -> v = u ) )
56	55	alrimiv 1781	. . . . . . . . . 10 |- ( v = u -> A. x ( x = y -> v = u ) )
57		equequ1 1875	. . . . . . . . . . . . 13 |- ( v = z -> ( v = u <-> z = u ) )
58		equequ2 1876	. . . . . . . . . . . . 13 |- ( u = w -> ( z = u <-> z = w ) )
59	57, 58	sylan9bb 714	. . . . . . . . . . . 12 |- ( ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
60	59	adantl 473	. . . . . . . . . . 11 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( v = u <-> z = w ) )
61		dveeq2-o 32568	. . . . . . . . . . . . . . 15 |- ( -. A. x x = z -> ( v = z -> A. x v = z ) )
62		dveeq2-o 32568	. . . . . . . . . . . . . . 15 |- ( -. A. x x = w -> ( u = w -> A. x u = w ) )
63	61, 62	im2anan9 853	. . . . . . . . . . . . . 14 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( ( v = z /\ u = w ) -> ( A. x v = z /\ A. x u = w ) ) )
64	63	imp 436	. . . . . . . . . . . . 13 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x v = z /\ A. x u = w ) )
65		19.26 1740	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) <-> ( A. x v = z /\ A. x u = w ) )
66	64, 65	sylibr 217	. . . . . . . . . . . 12 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> A. x ( v = z /\ u = w ) )
67		nfa1-o 32550	. . . . . . . . . . . . 13 |- F/ x A. x ( v = z /\ u = w )
68	59	sps-o 32543	. . . . . . . . . . . . . 14 |- ( A. x ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
69	68	imbi2d 323	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) -> ( ( x = y -> v = u ) <-> ( x = y -> z = w ) ) )
70	67, 69	albid 1983	. . . . . . . . . . . 12 |- ( A. x ( v = z /\ u = w ) -> ( A. x ( x = y -> v = u ) <-> A. x ( x = y -> z = w ) ) )
71	66, 70	syl 17	. . . . . . . . . . 11 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x ( x = y -> v = u ) <-> A. x ( x = y -> z = w ) ) )
72	60, 71	imbi12d 327	. . . . . . . . . 10 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( ( v = u -> A. x ( x = y -> v = u ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
73	56, 72	mpbii 216	. . . . . . . . 9 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
74	73	exp32 616	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( v = z -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
75	74	exlimdv 1787	. . . . . . 7 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( E. v v = z -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
76	54, 75	mpi 20	. . . . . 6 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
77	76	exlimdv 1787	. . . . 5 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( E. u u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
78	53, 77	mpi 20	. . . 4 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
79	78	a1d 25	. . 3 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
80	79	a1d 25	. 2 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
81	17, 35, 52, 80	4cases 964	1 |- ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   /\ wa 376   A.wal 1450   E.wex 1671

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-c5 32519  ax-c4 32520  ax-c7 32521  ax-c11 32523  ax-c9 32526

This theorem depends on definitions:  df-bi 190  df-an 378  df-ex 1672  df-nf 1676

This theorem is referenced by: (None)