Theorem ax12eq 34226

Description: Basis step for constructing a substitution instance of ax-c15 34174 without using ax-c15 34174. 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 1798	. . 3 |- ( A. x ( x = z /\ x = w ) <-> ( A. x x = z /\ A. x x = w ) )
2		equid 1939	. . . . . . . 8 |- x = x
3	2	a1i 11	. . . . . . 7 |- ( x = y -> x = x )
4	3	ax-gen 1722	. . . . . 6 |- A. x ( x = y -> x = x )
5	4	a1i 11	. . . . 5 |- ( x = x -> A. x ( x = y -> x = x ) )
6		equequ1 1952	. . . . . . . . 9 |- ( x = z -> ( x = x <-> z = x ) )
7		equequ2 1953	. . . . . . . . 9 |- ( x = w -> ( z = x <-> z = w ) )
8	6, 7	sylan9bb 736	. . . . . . . 8 |- ( ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
9	8	sps-o 34193	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
10		nfa1-o 34200	. . . . . . . 8 |- F/ x A. x ( x = z /\ x = w )
11	9	imbi2d 330	. . . . . . . 8 |- ( A. x ( x = z /\ x = w ) -> ( ( x = y -> x = x ) <-> ( x = y -> z = w ) ) )
12	10, 11	albid 2090	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( A. x ( x = y -> x = x ) <-> A. x ( x = y -> z = w ) ) )
13	9, 12	imbi12d 334	. . . . . 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 481	. . . . 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 223	. . . 4 |- ( ( A. x ( x = z /\ x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
16	15	exp32 631	. . 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 225	. 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 1952	. . . . . . 7 |- ( x = y -> ( x = w <-> y = w ) )
19	18	ad2antll 765	. . . . . 6 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w <-> y = w ) )
20		axc9 2302	. . . . . . . . 9 |- ( -. A. x x = y -> ( -. A. x x = w -> ( y = w -> A. x y = w ) ) )
21	20	impcom 446	. . . . . . . 8 |- ( ( -. A. x x = w /\ -. A. x x = y ) -> ( y = w -> A. x y = w ) )
22	21	adantrr 753	. . . . . . 7 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x y = w ) )
23		equtrr 1949	. . . . . . . 8 |- ( y = w -> ( x = y -> x = w ) )
24	23	alimi 1739	. . . . . . 7 |- ( A. x y = w -> A. x ( x = y -> x = w ) )
25	22, 24	syl6 35	. . . . . 6 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x ( x = y -> x = w ) ) )
26	19, 25	sylbid 230	. . . . 5 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w -> A. x ( x = y -> x = w ) ) )
27	26	adantll 750	. . . 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 1952	. . . . . . 7 |- ( x = z -> ( x = w <-> z = w ) )
29	28	sps-o 34193	. . . . . 6 |- ( A. x x = z -> ( x = w <-> z = w ) )
30	29	imbi2d 330	. . . . . . 7 |- ( A. x x = z -> ( ( x = y -> x = w ) <-> ( x = y -> z = w ) ) )
31	30	dral2-o 34215	. . . . . 6 |- ( A. x x = z -> ( A. x ( x = y -> x = w ) <-> A. x ( x = y -> z = w ) ) )
32	29, 31	imbi12d 334	. . . . 5 |- ( A. x x = z -> ( ( x = w -> A. x ( x = y -> x = w ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
33	32	ad2antrr 762	. . . 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 222	. . 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 631	. 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 1953	. . . . . . 7 |- ( x = y -> ( z = x <-> z = y ) )
37	36	ad2antll 765	. . . . . 6 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x <-> z = y ) )
38		axc9 2302	. . . . . . . . 9 |- ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
39	38	imp 445	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
40	39	adantrr 753	. . . . . . 7 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x z = y ) )
41	36	biimprcd 240	. . . . . . . 8 |- ( z = y -> ( x = y -> z = x ) )
42	41	alimi 1739	. . . . . . 7 |- ( A. x z = y -> A. x ( x = y -> z = x ) )
43	40, 42	syl6 35	. . . . . 6 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x ( x = y -> z = x ) ) )
44	37, 43	sylbid 230	. . . . 5 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x -> A. x ( x = y -> z = x ) ) )
45	44	adantlr 751	. . . 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 34193	. . . . . 6 |- ( A. x x = w -> ( z = x <-> z = w ) )
47	46	imbi2d 330	. . . . . . 7 |- ( A. x x = w -> ( ( x = y -> z = x ) <-> ( x = y -> z = w ) ) )
48	47	dral2-o 34215	. . . . . 6 |- ( A. x x = w -> ( A. x ( x = y -> z = x ) <-> A. x ( x = y -> z = w ) ) )
49	46, 48	imbi12d 334	. . . . 5 |- ( A. x x = w -> ( ( z = x -> A. x ( x = y -> z = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
50	49	ad2antlr 763	. . . 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 222	. . 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 631	. 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 1890	. . . . 5 |- E. u u = w
54		ax6ev 1890	. . . . . . 7 |- E. v v = z
55		ax-1 6	. . . . . . . . . . 11 |- ( v = u -> ( x = y -> v = u ) )
56	55	alrimiv 1855	. . . . . . . . . 10 |- ( v = u -> A. x ( x = y -> v = u ) )
57		equequ1 1952	. . . . . . . . . . . . 13 |- ( v = z -> ( v = u <-> z = u ) )
58		equequ2 1953	. . . . . . . . . . . . 13 |- ( u = w -> ( z = u <-> z = w ) )
59	57, 58	sylan9bb 736	. . . . . . . . . . . 12 |- ( ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
60	59	adantl 482	. . . . . . . . . . 11 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( v = u <-> z = w ) )
61		dveeq2-o 34218	. . . . . . . . . . . . . . 15 |- ( -. A. x x = z -> ( v = z -> A. x v = z ) )
62		dveeq2-o 34218	. . . . . . . . . . . . . . 15 |- ( -. A. x x = w -> ( u = w -> A. x u = w ) )
63	61, 62	im2anan9 880	. . . . . . . . . . . . . 14 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( ( v = z /\ u = w ) -> ( A. x v = z /\ A. x u = w ) ) )
64	63	imp 445	. . . . . . . . . . . . 13 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x v = z /\ A. x u = w ) )
65		19.26 1798	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) <-> ( A. x v = z /\ A. x u = w ) )
66	64, 65	sylibr 224	. . . . . . . . . . . 12 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> A. x ( v = z /\ u = w ) )
67		nfa1-o 34200	. . . . . . . . . . . . 13 |- F/ x A. x ( v = z /\ u = w )
68	59	sps-o 34193	. . . . . . . . . . . . . 14 |- ( A. x ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
69	68	imbi2d 330	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) -> ( ( x = y -> v = u ) <-> ( x = y -> z = w ) ) )
70	67, 69	albid 2090	. . . . . . . . . . . 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 334	. . . . . . . . . 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 223	. . . . . . . . 9 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
74	73	exp32 631	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( v = z -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
75	74	exlimdv 1861	. . . . . . 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 1861	. . . . 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 990	1 |- ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   A.wal 1481   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-c5 34168  ax-c4 34169  ax-c7 34170  ax-c10 34171  ax-c11 34172  ax-c9 34175

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710

This theorem is referenced by: (None)