Theorem ax12eq 2271

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

Assertion

Ref	Expression
ax12eq

Proof of Theorem ax12eq

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

Step	Hyp	Ref	Expression
1		19.26 1680	. . 3
2		equid 1791	. . . . . . . 8
3	2	a1i 11	. . . . . . 7
4	3	ax-gen 1618	. . . . . 6
5	4	a1i 11	. . . . 5
6		equequ1 1798	. . . . . . . . 9
7		equequ2 1799	. . . . . . . . 9
8	6, 7	sylan9bb 699	. . . . . . . 8
9	8	sps-o 2238	. . . . . . 7
10		nfa1-o 2245	. . . . . . . 8
11	9	imbi2d 316	. . . . . . . 8
12	10, 11	albid 1885	. . . . . . 7
13	9, 12	imbi12d 320	. . . . . 6
14	13	adantr 465	. . . . 5
15	5, 14	mpbii 211	. . . 4
16	15	exp32 605	. . 3
17	1, 16	sylbir 213	. 2
18		equequ1 1798	. . . . . . 7
19	18	ad2antll 728	. . . . . 6
20		axc9 2046	. . . . . . . . 9
21	20	impcom 430	. . . . . . . 8
22	21	adantrr 716	. . . . . . 7
23		equtrr 1797	. . . . . . . 8
24	23	alimi 1633	. . . . . . 7
25	22, 24	syl6 33	. . . . . 6
26	19, 25	sylbid 215	. . . . 5
27	26	adantll 713	. . . 4
28		equequ1 1798	. . . . . . 7
29	28	sps-o 2238	. . . . . 6
30	29	imbi2d 316	. . . . . . 7
31	30	dral2-o 2260	. . . . . 6
32	29, 31	imbi12d 320	. . . . 5
33	32	ad2antrr 725	. . . 4
34	27, 33	mpbid 210	. . 3
35	34	exp32 605	. 2
36		equequ2 1799	. . . . . . 7
37	36	ad2antll 728	. . . . . 6
38		axc9 2046	. . . . . . . . 9
39	38	imp 429	. . . . . . . 8
40	39	adantrr 716	. . . . . . 7
41	36	biimprcd 225	. . . . . . . 8
42	41	alimi 1633	. . . . . . 7
43	40, 42	syl6 33	. . . . . 6
44	37, 43	sylbid 215	. . . . 5
45	44	adantlr 714	. . . 4
46	7	sps-o 2238	. . . . . 6
47	46	imbi2d 316	. . . . . . 7
48	47	dral2-o 2260	. . . . . 6
49	46, 48	imbi12d 320	. . . . 5
50	49	ad2antlr 726	. . . 4
51	45, 50	mpbid 210	. . 3
52	51	exp32 605	. 2
53		ax6ev 1749	. . . . 5
54		ax6ev 1749	. . . . . . 7
55		ax-1 6	. . . . . . . . . . 11
56	55	alrimiv 1719	. . . . . . . . . 10
57		equequ1 1798	. . . . . . . . . . . . 13
58		equequ2 1799	. . . . . . . . . . . . 13
59	57, 58	sylan9bb 699	. . . . . . . . . . . 12
60	59	adantl 466	. . . . . . . . . . 11
61		dveeq2-o 2263	. . . . . . . . . . . . . . 15
62		dveeq2-o 2263	. . . . . . . . . . . . . . 15
63	61, 62	im2anan9 835	. . . . . . . . . . . . . 14
64	63	imp 429	. . . . . . . . . . . . 13
65		19.26 1680	. . . . . . . . . . . . 13
66	64, 65	sylibr 212	. . . . . . . . . . . 12
67		nfa1-o 2245	. . . . . . . . . . . . 13
68	59	sps-o 2238	. . . . . . . . . . . . . 14
69	68	imbi2d 316	. . . . . . . . . . . . 13
70	67, 69	albid 1885	. . . . . . . . . . . 12
71	66, 70	syl 16	. . . . . . . . . . 11
72	60, 71	imbi12d 320	. . . . . . . . . 10
73	56, 72	mpbii 211	. . . . . . . . 9
74	73	exp32 605	. . . . . . . 8
75	74	exlimdv 1724	. . . . . . 7
76	54, 75	mpi 17	. . . . . 6
77	76	exlimdv 1724	. . . . 5
78	53, 77	mpi 17	. . . 4
79	78	a1d 25	. . 3
80	79	a1d 25	. 2
81	17, 35, 52, 80	4cases 949	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-c5 2214  ax-c4 2215  ax-c7 2216  ax-c11 2218  ax-c9 2221

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617