Theorem ax12eq 32512

Description: Basis step for constructing a substitution instance of ax-c15 32461 without using ax-c15 32461. 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 1732	. . 3 |- ( A. x ( x = z /\ x = w ) <-> ( A. x x = z /\ A. x x = w ) )
2		equid 1855	. . . . . . . 8 |- x = x
3	2	a1i 11	. . . . . . 7 |- ( x = y -> x = x )
4	3	ax-gen 1669	. . . . . 6 |- A. x ( x = y -> x = x )
5	4	a1i 11	. . . . 5 |- ( x = x -> A. x ( x = y -> x = x ) )
6		equequ1 1867	. . . . . . . . 9 |- ( x = z -> ( x = x <-> z = x ) )
7		equequ2 1868	. . . . . . . . 9 |- ( x = w -> ( z = x <-> z = w ) )
8	6, 7	sylan9bb 706	. . . . . . . 8 |- ( ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
9	8	sps-o 32479	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
10		nfa1-o 32486	. . . . . . . 8 |- F/ x A. x ( x = z /\ x = w )
11	9	imbi2d 318	. . . . . . . 8 |- ( A. x ( x = z /\ x = w ) -> ( ( x = y -> x = x ) <-> ( x = y -> z = w ) ) )
12	10, 11	albid 1963	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( A. x ( x = y -> x = x ) <-> A. x ( x = y -> z = w ) ) )
13	9, 12	imbi12d 322	. . . . . 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 467	. . . . 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 215	. . . 4 |- ( ( A. x ( x = z /\ x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
16	15	exp32 610	. . 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 217	. 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 1867	. . . . . . 7 |- ( x = y -> ( x = w <-> y = w ) )
19	18	ad2antll 735	. . . . . 6 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w <-> y = w ) )
20		axc9 2140	. . . . . . . . 9 |- ( -. A. x x = y -> ( -. A. x x = w -> ( y = w -> A. x y = w ) ) )
21	20	impcom 432	. . . . . . . 8 |- ( ( -. A. x x = w /\ -. A. x x = y ) -> ( y = w -> A. x y = w ) )
22	21	adantrr 723	. . . . . . 7 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x y = w ) )
23		equtrr 1866	. . . . . . . 8 |- ( y = w -> ( x = y -> x = w ) )
24	23	alimi 1684	. . . . . . 7 |- ( A. x y = w -> A. x ( x = y -> x = w ) )
25	22, 24	syl6 34	. . . . . 6 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x ( x = y -> x = w ) ) )
26	19, 25	sylbid 219	. . . . 5 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w -> A. x ( x = y -> x = w ) ) )
27	26	adantll 720	. . . 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 1867	. . . . . . 7 |- ( x = z -> ( x = w <-> z = w ) )
29	28	sps-o 32479	. . . . . 6 |- ( A. x x = z -> ( x = w <-> z = w ) )
30	29	imbi2d 318	. . . . . . 7 |- ( A. x x = z -> ( ( x = y -> x = w ) <-> ( x = y -> z = w ) ) )
31	30	dral2-o 32501	. . . . . 6 |- ( A. x x = z -> ( A. x ( x = y -> x = w ) <-> A. x ( x = y -> z = w ) ) )
32	29, 31	imbi12d 322	. . . . 5 |- ( A. x x = z -> ( ( x = w -> A. x ( x = y -> x = w ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
33	32	ad2antrr 732	. . . 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 214	. . 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 610	. 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 1868	. . . . . . 7 |- ( x = y -> ( z = x <-> z = y ) )
37	36	ad2antll 735	. . . . . 6 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x <-> z = y ) )
38		axc9 2140	. . . . . . . . 9 |- ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
39	38	imp 431	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
40	39	adantrr 723	. . . . . . 7 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x z = y ) )
41	36	biimprcd 229	. . . . . . . 8 |- ( z = y -> ( x = y -> z = x ) )
42	41	alimi 1684	. . . . . . 7 |- ( A. x z = y -> A. x ( x = y -> z = x ) )
43	40, 42	syl6 34	. . . . . 6 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x ( x = y -> z = x ) ) )
44	37, 43	sylbid 219	. . . . 5 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x -> A. x ( x = y -> z = x ) ) )
45	44	adantlr 721	. . . 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 32479	. . . . . 6 |- ( A. x x = w -> ( z = x <-> z = w ) )
47	46	imbi2d 318	. . . . . . 7 |- ( A. x x = w -> ( ( x = y -> z = x ) <-> ( x = y -> z = w ) ) )
48	47	dral2-o 32501	. . . . . 6 |- ( A. x x = w -> ( A. x ( x = y -> z = x ) <-> A. x ( x = y -> z = w ) ) )
49	46, 48	imbi12d 322	. . . . 5 |- ( A. x x = w -> ( ( z = x -> A. x ( x = y -> z = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
50	49	ad2antlr 733	. . . 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 214	. . 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 610	. 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 1807	. . . . 5 |- E. u u = w
54		ax6ev 1807	. . . . . . 7 |- E. v v = z
55		ax-1 6	. . . . . . . . . . 11 |- ( v = u -> ( x = y -> v = u ) )
56	55	alrimiv 1773	. . . . . . . . . 10 |- ( v = u -> A. x ( x = y -> v = u ) )
57		equequ1 1867	. . . . . . . . . . . . 13 |- ( v = z -> ( v = u <-> z = u ) )
58		equequ2 1868	. . . . . . . . . . . . 13 |- ( u = w -> ( z = u <-> z = w ) )
59	57, 58	sylan9bb 706	. . . . . . . . . . . 12 |- ( ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
60	59	adantl 468	. . . . . . . . . . 11 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( v = u <-> z = w ) )
61		dveeq2-o 32504	. . . . . . . . . . . . . . 15 |- ( -. A. x x = z -> ( v = z -> A. x v = z ) )
62		dveeq2-o 32504	. . . . . . . . . . . . . . 15 |- ( -. A. x x = w -> ( u = w -> A. x u = w ) )
63	61, 62	im2anan9 846	. . . . . . . . . . . . . 14 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( ( v = z /\ u = w ) -> ( A. x v = z /\ A. x u = w ) ) )
64	63	imp 431	. . . . . . . . . . . . 13 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x v = z /\ A. x u = w ) )
65		19.26 1732	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) <-> ( A. x v = z /\ A. x u = w ) )
66	64, 65	sylibr 216	. . . . . . . . . . . 12 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> A. x ( v = z /\ u = w ) )
67		nfa1-o 32486	. . . . . . . . . . . . 13 |- F/ x A. x ( v = z /\ u = w )
68	59	sps-o 32479	. . . . . . . . . . . . . 14 |- ( A. x ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
69	68	imbi2d 318	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) -> ( ( x = y -> v = u ) <-> ( x = y -> z = w ) ) )
70	67, 69	albid 1963	. . . . . . . . . . . 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 322	. . . . . . . . . 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 215	. . . . . . . . 9 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
74	73	exp32 610	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( v = z -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
75	74	exlimdv 1779	. . . . . . 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 1779	. . . . 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 26	. . 3 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
80	79	a1d 26	. 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 960	1 |- ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 188   /\ wa 371   A.wal 1442   E.wex 1663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-c5 32455  ax-c4 32456  ax-c7 32457  ax-c11 32459  ax-c9 32462

This theorem depends on definitions:  df-bi 189  df-an 373  df-ex 1664  df-nf 1668

This theorem is referenced by: (None)