Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem ax11eq 1356

Description: Basis step for constructing a substitution instance of ax-11o 1213 without using ax-11o 1213. Atomic formula for equality predicate.

Assertion

Ref	Expression
ax11eq

---

Proof of Theorem ax11eq

Step	Hyp	Ref	Expression
1		19.26 1063	. . 3
2		equid 1122	. . . . . . . 8
3	2	a1i 8	. . . . . . 7
4	3	ax-gen 960	. . . . . 6
5	4	a1i 8	. . . . 5
6		equequ1 1130	. . . . . . . . 9
7		equequ2 1131	. . . . . . . . 9
8	6, 7	sylan9bb 538	. . . . . . . 8
9	8	a4s 981	. . . . . . 7
10		hba1 1000	. . . . . . . 8
11	9	imbi2d 610	. . . . . . . 8
12	10, 11	albid 1100	. . . . . . 7
13	9, 12	imbi12d 624	. . . . . 6
14	13	adantr 389	. . . . 5
15	5, 14	mpbii 193	. . . 4
16	15	exp32 377	. . 3
17	1, 16	sylbir 201	. 2
18		equequ1 1130	. . . . . . 7
19	18	ad2antll 407	. . . . . 6
20		ax-12 965	. . . . . . . . 9
21	20	impcom 351	. . . . . . . 8
22	21	adantrr 395	. . . . . . 7
23		equtrr 1128	. . . . . . . 8
24	23	19.20i 989	. . . . . . 7
25	22, 24	syl6 22	. . . . . 6
26	19, 25	sylbid 203	. . . . 5
27	26	adantll 392	. . . 4
28		equequ1 1130	. . . . . . 7
29	28	a4s 981	. . . . . 6
30	29	imbi2d 610	. . . . . . 7
31	30	dral2 1151	. . . . . 6
32	29, 31	imbi12d 624	. . . . 5
33	32	ad2antrr 404	. . . 4
34	27, 33	mpbid 195	. . 3
35	34	exp32 377	. 2
36		equequ2 1131	. . . . . . 7
37	36	ad2antll 407	. . . . . 6
38		ax-12 965	. . . . . . . . 9
39	38	imp 350	. . . . . . . 8
40	39	adantrr 395	. . . . . . 7
41	36	biimprcd 156	. . . . . . . 8
42	41	19.20i 989	. . . . . . 7
43	40, 42	syl6 22	. . . . . 6
44	37, 43	sylbid 203	. . . . 5
45	44	adantlr 393	. . . 4
46	7	a4s 981	. . . . . 6
47	46	imbi2d 610	. . . . . . 7
48	47	dral2 1151	. . . . . 6
49	46, 48	imbi12d 624	. . . . 5
50	49	ad2antlr 405	. . . 4
51	45, 50	mpbid 195	. . 3
52	51	exp32 377	. 2
53		a9e 1121	. . . . 5
54		a9e 1121	. . . . . . 7
55		ax-1 4	. . . . . . . . . . 11
56	55	19.21aiv 1281	. . . . . . . . . 10
57		equequ1 1130	. . . . . . . . . . . . 13
58		equequ2 1131	. . . . . . . . . . . . 13
59	57, 58	sylan9bb 538	. . . . . . . . . . . 12
60	59	adantl 388	. . . . . . . . . . 11
61		dveeq2 1208	. . . . . . . . . . . . . . 15
62		dveeq2 1208	. . . . . . . . . . . . . . 15
63	61, 62	im2anan9 561	. . . . . . . . . . . . . 14