rdglem2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem rdglem2 3938

Description: Lemma used with the recursive definition generator. This is a trivial lemma that just changes bound variables for later use.

**Assertion**
Ref	Expression
rdglem2	$/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$

**Proof of Theorem rdglem2**
Step	Hyp	Ref	Expression
1		opeq1 2487	. . . . . . 7
2	1	eqeq2d 1486	. . . . . 6
3		eqeq1 1481	. . . . . . . 8
4	3	anbi1d 617	. . . . . . 7 $/\$ $/\$
5		dmeq 3311	. . . . . . . . . . 11
6		limeq 2960	. . . . . . . . . . 11
7	5, 6	syl 10	. . . . . . . . . 10
8	3, 7	orbi12d 627	. . . . . . . . 9 $\/$ $\/$
9	8	negbid 611	. . . . . . . 8 $\/$ $\/$
10		unieq 2510	. . . . . . . . . . . 12
11		fveq2 3724	. . . . . . . . . . . 12
12	5, 10, 11	3syl 20	. . . . . . . . . . 11
13		fveq1 3723	. . . . . . . . . . 11
14	12, 13	eqtrd 1507	. . . . . . . . . 10
15	14	fveq2d 3728	. . . . . . . . 9
16	15	eqeq2d 1486	. . . . . . . 8
17	9, 16	anbi12d 628	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
18		rneq 3339	. . . . . . . . . 10
19	18	unieqd 2512	. . . . . . . . 9
20	19	eqeq2d 1486	. . . . . . . 8
21	7, 20	anbi12d 628	. . . . . . 7 $/\$ $/\$
22	4, 17, 21	3orbi123d 892	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
23	2, 22	anbi12d 628	. . . . 5 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
24	23	exbidv 1279	. . . 4 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
25	24	cbvexv 1315	. . 3 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
26	25	abbii 1575	. 2 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
27		df-opab 2667	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
28		df-opab 2667	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
29	26, 27, 28	3eqtr4 1505	1 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 2

wb 146 $\/$ wo 222 $/\$ wa 223 $\/$ w3o 774

wceq 956

wex 980

cab 1463

c0 2280

cop 2411

cuni 2503

copab 2666

wlim 2949

cdm 3170

crn 3171

cfv 3182

This theorem is referenced by: rdgval 3940 rdg0 3941 rdgsuc 3942 rdglim 3943

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 962 ax-gen 963 ax-8 964 ax-10 966 ax-11 967 ax-12 968 ax-13 969 ax-14 970 ax-17 971 ax-4 973 ax-5o 975 ax-6o 978 ax-9o 1123 ax-10o 1140 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-sep 2703 ax-pow 2742 ax-pr 2779

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 776 df-3an 777 df-ex 981 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1587 df-ral 1649 df-rex 1650 df-v 1812 df-dif 2049 df-un 2050 df-in 2051 df-ss 2053 df-nul 2281 df-pw 2402 df-sn 2412 df-pr 2413 df-op 2416 df-uni 2504 df-br 2620 df-opab 2667 df-tr 2681 df-po 2840 df-so 2850 df-fr 2917 df-we 2934 df-ord 2951 df-lim 2953 df-xp 3184 df-cnv 3186 df-dm 3188 df-rn 3189 df-res 3190 df-ima 3191 df-fv 3198