Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem acdc5 7443

Description: A more general version of acdc 7445 that has an initial value and where the function depends on .

Hypothesis

Ref	Expression
acdc5.1

Assertion

Ref	Expression
acdc5

Distinct variable groups:   ,,   ,,   ,

---

Proof of Theorem acdc5

Step	Hyp	Ref	Expression
1		eqeq2 1481	. . . . . 6
2	1	3anbi2d 896	. . . . 5
3	2	exbidv 1277	. . . 4
4	3	imbi2d 611	. . 3
5		acdc5.1	. . . . 5
6	5	weth 4767	. . . 4
7		eleq1 1531	. . . . . . . . . . . 12
8		eleq1 1531	. . . . . . . . . . . 12
9	7, 8	bi2anan9 631	. . . . . . . . . . 11
10		opreq12 3961	. . . . . . . . . . . . . . . 16
11	10	ancoms 436	. . . . . . . . . . . . . . 15
12		rabeq 1805	. . . . . . . . . . . . . . . 16
13		raleq1 1783	. . . . . . . . . . . . . . . . 17
14	13	rabbisdv 1803	. . . . . . . . . . . . . . . 16
15	12, 14	eqtrd 1504	. . . . . . . . . . . . . . 15
16	11, 15	syl 10	. . . . . . . . . . . . . 14
17		breq2 2618	. . . . . . . . . . . . . . . . . 18
18	17	negbid 610	. . . . . . . . . . . . . . . . 17
19	18	ralbidv 1660	. . . . . . . . . . . . . . . 16
20		breq1 2617	. . . . . . . . . . . . . . . . . 18
21	20	negbid 610	. . . . . . . . . . . . . . . . 17
22	21	cbvralv 1796	. . . . . . . . . . . . . . . 16
23	19, 22	syl6bb 535	. . . . . . . . . . . . . . 15
24	23	cbvrabv 1907	. . . . . . . . . . . . . 14
25	16, 24	syl6eq 1520	. . . . . . . . . . . . 13
26	25	unieqd 2507	. . . . . . . . . . . 12
27	26	eqeq2d 1483	. . . . . . . . . . 11
28	9, 27	anbi12d 627	. . . . . . . . . 10
29	28	cbvoprab12v 3990	. . . . . . . . 9
30		eqeq1 1478	. . . . . . . . . . 11
31	30	anbi2d 615	. . . . . . . . . 10
32	31	cbvoprab3v 3991	. . . . . . . . 9
33	29, 32	eqtr 1492	. . . . . . . 8
34		eqid 1473	. . . . . . . 8
35	5, 33, 34	acdc5lem2 7442	. . . . . . 7