rdglem2 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem rdglem2 3929

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 2483	. . . . . . 7
2	1	eqeq2d 1483	. . . . . 6
3		eqeq1 1478	. . . . . . . 8
4	3	anbi1d 616	. . . . . . 7 $/\$ $/\$
5		dmeq 3306	. . . . . . . . . . 11
6		limeq 2955	. . . . . . . . . . 11
7	5, 6	syl 10	. . . . . . . . . 10
8	3, 7	orbi12d 626	. . . . . . . . 9 $\/$ $\/$
9	8	negbid 610	. . . . . . . 8 $\/$ $\/$
10		unieq 2505	. . . . . . . . . . . 12
11		fveq2 3715	. . . . . . . . . . . 12
12	5, 10, 11	3syl 20	. . . . . . . . . . 11
13		fveq1 3714	. . . . . . . . . . 11
14	12, 13	eqtrd 1504	. . . . . . . . . 10
15	14	fveq2d 3719	. . . . . . . . 9
16	15	eqeq2d 1483	. . . . . . . 8
17	9, 16	anbi12d 627	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
18		rneq 3334	. . . . . . . . . 10
19	18	unieqd 2507	. . . . . . . . 9
20	19	eqeq2d 1483	. . . . . . . 8
21	7, 20	anbi12d 627	. . . . . . 7 $/\$ $/\$
22	4, 17, 21	3orbi123d 890	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
23	2, 22	anbi12d 627	. . . . 5 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
24	23	exbidv 1277	. . . 4 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
25	24	cbvexv 1313	. . 3 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
26	25	abbii 1572	. 2 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
27		df-opab 2662	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
28		df-opab 2662	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
29	26, 27, 28	3eqtr4 1502	1 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 2

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

wceq 954

wex 978

cab 1461

c0 2276

cop 2407

cuni 2498

copab 2661

wlim 2944

cdm 3165

crn 3166

cfv 3177

This theorem is referenced by: rdgval 3931 rdg0 3932 rdgsuc 3933 rdglim 3934

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-10 964 ax-11 965 ax-12 966 ax-13 967 ax-14 968 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 ax-sep 2698 ax-pow 2737 ax-pr 2774

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 979 df-sb 1170 df-eu 1380 df-mo 1381 df-clab 1462 df-cleq 1467 df-clel 1470 df-ne 1584 df-ral 1646 df-rex 1647 df-v 1808 df-dif 2045 df-un 2046 df-in 2047 df-ss 2049 df-nul 2277 df-pw 2398 df-sn 2408 df-pr 2409 df-op 2412 df-uni 2499 df-br 2615 df-opab 2662 df-tr 2676 df-po 2835 df-so 2845 df-fr 2912 df-we 2929 df-ord 2946 df-lim 2948 df-xp 3179 df-cnv 3181 df-dm 3183 df-rn 3184 df-res 3185 df-ima 3186 df-fv 3193