Theorem ax12el 2272

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

Assertion

Ref	Expression
ax12el

Proof of Theorem ax12el

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

Step	Hyp	Ref	Expression
1		19.26 1680	. . 3
2		elequ1 1821	. . . . . . . . 9
3		elequ2 1823	. . . . . . . . 9
4	2, 3	bitrd 253	. . . . . . . 8
5	4	adantl 466	. . . . . . 7
6		ax-5 1704	. . . . . . . . . 10
7		ax-5 1704	. . . . . . . . . 10
8		elequ1 1821	. . . . . . . . . . 11
9		elequ2 1823	. . . . . . . . . . 11
10	8, 9	bitrd 253	. . . . . . . . . 10
11	6, 7, 10	dvelimf-o 2259	. . . . . . . . 9
12	4	biimprcd 225	. . . . . . . . . 10
13	12	alimi 1633	. . . . . . . . 9
14	11, 13	syl6 33	. . . . . . . 8
15	14	adantr 465	. . . . . . 7
16	5, 15	sylbid 215	. . . . . 6
17	16	adantl 466	. . . . 5
18		elequ1 1821	. . . . . . . . 9
19		elequ2 1823	. . . . . . . . 9
20	18, 19	sylan9bb 699	. . . . . . . 8
21	20	sps-o 2238	. . . . . . 7
22		nfa1-o 2245	. . . . . . . 8
23	21	imbi2d 316	. . . . . . . 8
24	22, 23	albid 1885	. . . . . . 7
25	21, 24	imbi12d 320	. . . . . 6
26	25	adantr 465	. . . . 5
27	17, 26	mpbid 210	. . . 4
28	27	exp32 605	. . 3
29	1, 28	sylbir 213	. 2
30		elequ1 1821	. . . . . . 7
31	30	ad2antll 728	. . . . . 6
32		ax-c14 2222	. . . . . . . . 9
33	32	impcom 430	. . . . . . . 8
34	33	adantrr 716	. . . . . . 7
35	30	biimprcd 225	. . . . . . . 8
36	35	alimi 1633	. . . . . . 7
37	34, 36	syl6 33	. . . . . 6
38	31, 37	sylbid 215	. . . . 5
39	38	adantll 713	. . . 4
40		elequ1 1821	. . . . . . 7
41	40	sps-o 2238	. . . . . 6
42	41	imbi2d 316	. . . . . . 7
43	42	dral2-o 2260	. . . . . 6
44	41, 43	imbi12d 320	. . . . 5
45	44	ad2antrr 725	. . . 4
46	39, 45	mpbid 210	. . 3
47	46	exp32 605	. 2
48		elequ2 1823	. . . . . . 7
49	48	ad2antll 728	. . . . . 6
50		ax-c14 2222	. . . . . . . . 9
51	50	imp 429	. . . . . . . 8
52	51	adantrr 716	. . . . . . 7
53	48	biimprcd 225	. . . . . . . 8
54	53	alimi 1633	. . . . . . 7
55	52, 54	syl6 33	. . . . . 6
56	49, 55	sylbid 215	. . . . 5
57	56	adantlr 714	. . . 4
58	19	sps-o 2238	. . . . . 6
59	58	imbi2d 316	. . . . . . 7
60	59	dral2-o 2260	. . . . . 6
61	58, 60	imbi12d 320	. . . . 5
62	61	ad2antlr 726	. . . 4
63	57, 62	mpbid 210	. . 3
64	63	exp32 605	. 2
65		ax6ev 1749	. . . . 5
66		ax6ev 1749	. . . . . . 7
67		ax-1 6	. . . . . . . . . . 11
68	67	alrimiv 1719	. . . . . . . . . 10
69		elequ1 1821	. . . . . . . . . . . . 13
70		elequ2 1823	. . . . . . . . . . . . 13
71	69, 70	sylan9bb 699	. . . . . . . . . . . 12
72	71	adantl 466	. . . . . . . . . . 11
73		dveeq2-o 2263	. . . . . . . . . . . . . . 15
74		dveeq2-o 2263	. . . . . . . . . . . . . . 15
75	73, 74	im2anan9 835	. . . . . . . . . . . . . 14
76	75	imp 429	. . . . . . . . . . . . 13
77		19.26 1680	. . . . . . . . . . . . 13
78	76, 77	sylibr 212	. . . . . . . . . . . 12
79		nfa1-o 2245	. . . . . . . . . . . . 13
80	71	sps-o 2238	. . . . . . . . . . . . . 14
81	80	imbi2d 316	. . . . . . . . . . . . 13
82	79, 81	albid 1885	. . . . . . . . . . . 12
83	78, 82	syl 16	. . . . . . . . . . 11
84	72, 83	imbi12d 320	. . . . . . . . . 10
85	68, 84	mpbii 211	. . . . . . . . 9
86	85	exp32 605	. . . . . . . 8
87	86	exlimdv 1724	. . . . . . 7
88	66, 87	mpi 17	. . . . . 6
89	88	exlimdv 1724	. . . . 5
90	65, 89	mpi 17	. . . 4
91	90	a1d 25	. . 3
92	91	a1d 25	. 2
93	29, 47, 64, 92	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-8 1820  ax-9 1822  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  ax-c14 2222

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