Theorem ax12eq 2273

Description: Basis step for constructing a substitution instance of ax-c15 2222 without using ax-c15 2222. 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 1685	. . 3 |- ( A. x ( x = z /\ x = w ) <-> ( A. x x = z /\ A. x x = w ) )
2		equid 1796	. . . . . . . 8 |- x = x
3	2	a1i 11	. . . . . . 7 |- ( x = y -> x = x )
4	3	ax-gen 1623	. . . . . 6 |- A. x ( x = y -> x = x )
5	4	a1i 11	. . . . 5 |- ( x = x -> A. x ( x = y -> x = x ) )
6		equequ1 1803	. . . . . . . . 9 |- ( x = z -> ( x = x <-> z = x ) )
7		equequ2 1804	. . . . . . . . 9 |- ( x = w -> ( z = x <-> z = w ) )
8	6, 7	sylan9bb 697	. . . . . . . 8 |- ( ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
9	8	sps-o 2240	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
10		nfa1-o 2247	. . . . . . . 8 |- F/ x A. x ( x = z /\ x = w )
11	9	imbi2d 314	. . . . . . . 8 |- ( A. x ( x = z /\ x = w ) -> ( ( x = y -> x = x ) <-> ( x = y -> z = w ) ) )
12	10, 11	albid 1890	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( A. x ( x = y -> x = x ) <-> A. x ( x = y -> z = w ) ) )
13	9, 12	imbi12d 318	. . . . . 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 463	. . . . 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 211	. . . 4 |- ( ( A. x ( x = z /\ x = w ) /\ ( -. A. x x = y /\ x = y ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
16	15	exp32 603	. . 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 213	. 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 1803	. . . . . . 7 |- ( x = y -> ( x = w <-> y = w ) )
19	18	ad2antll 726	. . . . . 6 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w <-> y = w ) )
20		axc9 2050	. . . . . . . . 9 |- ( -. A. x x = y -> ( -. A. x x = w -> ( y = w -> A. x y = w ) ) )
21	20	impcom 428	. . . . . . . 8 |- ( ( -. A. x x = w /\ -. A. x x = y ) -> ( y = w -> A. x y = w ) )
22	21	adantrr 714	. . . . . . 7 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x y = w ) )
23		equtrr 1802	. . . . . . . 8 |- ( y = w -> ( x = y -> x = w ) )
24	23	alimi 1638	. . . . . . 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 215	. . . . 5 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w -> A. x ( x = y -> x = w ) ) )
27	26	adantll 711	. . . 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 1803	. . . . . . 7 |- ( x = z -> ( x = w <-> z = w ) )
29	28	sps-o 2240	. . . . . 6 |- ( A. x x = z -> ( x = w <-> z = w ) )
30	29	imbi2d 314	. . . . . . 7 |- ( A. x x = z -> ( ( x = y -> x = w ) <-> ( x = y -> z = w ) ) )
31	30	dral2-o 2262	. . . . . 6 |- ( A. x x = z -> ( A. x ( x = y -> x = w ) <-> A. x ( x = y -> z = w ) ) )
32	29, 31	imbi12d 318	. . . . 5 |- ( A. x x = z -> ( ( x = w -> A. x ( x = y -> x = w ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
33	32	ad2antrr 723	. . . 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 210	. . 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 603	. 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 1804	. . . . . . 7 |- ( x = y -> ( z = x <-> z = y ) )
37	36	ad2antll 726	. . . . . 6 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x <-> z = y ) )
38		axc9 2050	. . . . . . . . 9 |- ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
39	38	imp 427	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
40	39	adantrr 714	. . . . . . 7 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = y -> A. x z = y ) )
41	36	biimprcd 225	. . . . . . . 8 |- ( z = y -> ( x = y -> z = x ) )
42	41	alimi 1638	. . . . . . 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 215	. . . . 5 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x -> A. x ( x = y -> z = x ) ) )
45	44	adantlr 712	. . . 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 2240	. . . . . 6 |- ( A. x x = w -> ( z = x <-> z = w ) )
47	46	imbi2d 314	. . . . . . 7 |- ( A. x x = w -> ( ( x = y -> z = x ) <-> ( x = y -> z = w ) ) )
48	47	dral2-o 2262	. . . . . 6 |- ( A. x x = w -> ( A. x ( x = y -> z = x ) <-> A. x ( x = y -> z = w ) ) )
49	46, 48	imbi12d 318	. . . . 5 |- ( A. x x = w -> ( ( z = x -> A. x ( x = y -> z = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
50	49	ad2antlr 724	. . . 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 210	. . 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 603	. 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 1754	. . . . 5 |- E. u u = w
54		ax6ev 1754	. . . . . . 7 |- E. v v = z
55		ax-1 6	. . . . . . . . . . 11 |- ( v = u -> ( x = y -> v = u ) )
56	55	alrimiv 1724	. . . . . . . . . 10 |- ( v = u -> A. x ( x = y -> v = u ) )
57		equequ1 1803	. . . . . . . . . . . . 13 |- ( v = z -> ( v = u <-> z = u ) )
58		equequ2 1804	. . . . . . . . . . . . 13 |- ( u = w -> ( z = u <-> z = w ) )
59	57, 58	sylan9bb 697	. . . . . . . . . . . 12 |- ( ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
60	59	adantl 464	. . . . . . . . . . 11 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( v = u <-> z = w ) )
61		dveeq2-o 2265	. . . . . . . . . . . . . . 15 |- ( -. A. x x = z -> ( v = z -> A. x v = z ) )
62		dveeq2-o 2265	. . . . . . . . . . . . . . 15 |- ( -. A. x x = w -> ( u = w -> A. x u = w ) )
63	61, 62	im2anan9 833	. . . . . . . . . . . . . 14 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( ( v = z /\ u = w ) -> ( A. x v = z /\ A. x u = w ) ) )
64	63	imp 427	. . . . . . . . . . . . 13 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x v = z /\ A. x u = w ) )
65		19.26 1685	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) <-> ( A. x v = z /\ A. x u = w ) )
66	64, 65	sylibr 212	. . . . . . . . . . . 12 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> A. x ( v = z /\ u = w ) )
67		nfa1-o 2247	. . . . . . . . . . . . 13 |- F/ x A. x ( v = z /\ u = w )
68	59	sps-o 2240	. . . . . . . . . . . . . 14 |- ( A. x ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
69	68	imbi2d 314	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) -> ( ( x = y -> v = u ) <-> ( x = y -> z = w ) ) )
70	67, 69	albid 1890	. . . . . . . . . . . 12 |- ( A. x ( v = z /\ u = w ) -> ( A. x ( x = y -> v = u ) <-> A. x ( x = y -> z = w ) ) )
71	66, 70	syl 16	. . . . . . . . . . 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 318	. . . . . . . . . 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 211	. . . . . . . . 9 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( z = w -> A. x ( x = y -> z = w ) ) )
74	73	exp32 603	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( v = z -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
75	74	exlimdv 1729	. . . . . . 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 17	. . . . . 6 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) )
77	76	exlimdv 1729	. . . . 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 17	. . . 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 947	1 |- ( -. A. x x = y -> ( x = y -> ( z = w -> A. x ( x = y -> z = w ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 184   /\ wa 367   A.wal 1396   E.wex 1617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-c5 2216  ax-c4 2217  ax-c7 2218  ax-c11 2220  ax-c9 2223

This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-nf 1622

This theorem is referenced by: (None)