Theorem ax12eq 2255

Description: Basis step for constructing a substitution instance of ax-c15 2204 without using ax-c15 2204. 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 1665	. . 3 |- ( A. x ( x = z /\ x = w ) <-> ( A. x x = z /\ A. x x = w ) )
2		equid 1775	. . . . . . . 8 |- x = x
3	2	a1i 11	. . . . . . 7 |- ( x = y -> x = x )
4	3	ax-gen 1603	. . . . . 6 |- A. x ( x = y -> x = x )
5	4	a1i 11	. . . . 5 |- ( x = x -> A. x ( x = y -> x = x ) )
6		equequ1 1782	. . . . . . . . 9 |- ( x = z -> ( x = x <-> z = x ) )
7		equequ2 1783	. . . . . . . . 9 |- ( x = w -> ( z = x <-> z = w ) )
8	6, 7	sylan9bb 699	. . . . . . . 8 |- ( ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
9	8	sps-o 2222	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( x = x <-> z = w ) )
10		nfa1-o 2229	. . . . . . . 8 |- F/ x A. x ( x = z /\ x = w )
11	9	imbi2d 316	. . . . . . . 8 |- ( A. x ( x = z /\ x = w ) -> ( ( x = y -> x = x ) <-> ( x = y -> z = w ) ) )
12	10, 11	albid 1869	. . . . . . 7 |- ( A. x ( x = z /\ x = w ) -> ( A. x ( x = y -> x = x ) <-> A. x ( x = y -> z = w ) ) )
13	9, 12	imbi12d 320	. . . . . 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 465	. . . . 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 605	. . 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 1782	. . . . . . 7 |- ( x = y -> ( x = w <-> y = w ) )
19	18	ad2antll 728	. . . . . 6 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( x = w <-> y = w ) )
20		axc9 2030	. . . . . . . . 9 |- ( -. A. x x = y -> ( -. A. x x = w -> ( y = w -> A. x y = w ) ) )
21	20	impcom 430	. . . . . . . 8 |- ( ( -. A. x x = w /\ -. A. x x = y ) -> ( y = w -> A. x y = w ) )
22	21	adantrr 716	. . . . . . 7 |- ( ( -. A. x x = w /\ ( -. A. x x = y /\ x = y ) ) -> ( y = w -> A. x y = w ) )
23		equtrr 1781	. . . . . . . 8 |- ( y = w -> ( x = y -> x = w ) )
24	23	alimi 1618	. . . . . . 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 713	. . . 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 1782	. . . . . . 7 |- ( x = z -> ( x = w <-> z = w ) )
29	28	sps-o 2222	. . . . . 6 |- ( A. x x = z -> ( x = w <-> z = w ) )
30	29	imbi2d 316	. . . . . . 7 |- ( A. x x = z -> ( ( x = y -> x = w ) <-> ( x = y -> z = w ) ) )
31	30	dral2-o 2244	. . . . . 6 |- ( A. x x = z -> ( A. x ( x = y -> x = w ) <-> A. x ( x = y -> z = w ) ) )
32	29, 31	imbi12d 320	. . . . 5 |- ( A. x x = z -> ( ( x = w -> A. x ( x = y -> x = w ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
33	32	ad2antrr 725	. . . 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 605	. 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 1783	. . . . . . 7 |- ( x = y -> ( z = x <-> z = y ) )
37	36	ad2antll 728	. . . . . 6 |- ( ( -. A. x x = z /\ ( -. A. x x = y /\ x = y ) ) -> ( z = x <-> z = y ) )
38		axc9 2030	. . . . . . . . 9 |- ( -. A. x x = z -> ( -. A. x x = y -> ( z = y -> A. x z = y ) ) )
39	38	imp 429	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = y ) -> ( z = y -> A. x z = y ) )
40	39	adantrr 716	. . . . . . 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 1618	. . . . . . 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 714	. . . 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 2222	. . . . . 6 |- ( A. x x = w -> ( z = x <-> z = w ) )
47	46	imbi2d 316	. . . . . . 7 |- ( A. x x = w -> ( ( x = y -> z = x ) <-> ( x = y -> z = w ) ) )
48	47	dral2-o 2244	. . . . . 6 |- ( A. x x = w -> ( A. x ( x = y -> z = x ) <-> A. x ( x = y -> z = w ) ) )
49	46, 48	imbi12d 320	. . . . 5 |- ( A. x x = w -> ( ( z = x -> A. x ( x = y -> z = x ) ) <-> ( z = w -> A. x ( x = y -> z = w ) ) ) )
50	49	ad2antlr 726	. . . 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 605	. 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 1734	. . . . 5 |- E. u u = w
54		ax6ev 1734	. . . . . . 7 |- E. v v = z
55		ax-1 6	. . . . . . . . . . 11 |- ( v = u -> ( x = y -> v = u ) )
56	55	alrimiv 1704	. . . . . . . . . 10 |- ( v = u -> A. x ( x = y -> v = u ) )
57		equequ1 1782	. . . . . . . . . . . . 13 |- ( v = z -> ( v = u <-> z = u ) )
58		equequ2 1783	. . . . . . . . . . . . 13 |- ( u = w -> ( z = u <-> z = w ) )
59	57, 58	sylan9bb 699	. . . . . . . . . . . 12 |- ( ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
60	59	adantl 466	. . . . . . . . . . 11 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( v = u <-> z = w ) )
61		dveeq2-o 2247	. . . . . . . . . . . . . . 15 |- ( -. A. x x = z -> ( v = z -> A. x v = z ) )
62		dveeq2-o 2247	. . . . . . . . . . . . . . 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 429	. . . . . . . . . . . . 13 |- ( ( ( -. A. x x = z /\ -. A. x x = w ) /\ ( v = z /\ u = w ) ) -> ( A. x v = z /\ A. x u = w ) )
65		19.26 1665	. . . . . . . . . . . . 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 2229	. . . . . . . . . . . . 13 |- F/ x A. x ( v = z /\ u = w )
68	59	sps-o 2222	. . . . . . . . . . . . . 14 |- ( A. x ( v = z /\ u = w ) -> ( v = u <-> z = w ) )
69	68	imbi2d 316	. . . . . . . . . . . . 13 |- ( A. x ( v = z /\ u = w ) -> ( ( x = y -> v = u ) <-> ( x = y -> z = w ) ) )
70	67, 69	albid 1869	. . . . . . . . . . . 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 320	. . . . . . . . . 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 605	. . . . . . . 8 |- ( ( -. A. x x = z /\ -. A. x x = w ) -> ( v = z -> ( u = w -> ( z = w -> A. x ( x = y -> z = w ) ) ) ) )
75	74	exlimdv 1709	. . . . . . 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 1709	. . . . 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 369   A.wal 1379   E.wex 1597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-c5 2198  ax-c4 2199  ax-c7 2200  ax-c11 2202  ax-c9 2205

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1598  df-nf 1602

This theorem is referenced by: (None)