Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem rdglem2 2976

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	$/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$

Distinct variable group(s):

**Proof of Theorem rdglem2**
Step	Hyp	Ref	Expression
1		opeq1 1876	. . . . . . 7
2	1	cleq2d 1112	. . . . . 6
3		cleq1 1107	. . . . . . . 8
4	3	anbi1d 469	. . . . . . 7 $/\$ $/\$
5		dmeq 2531	. . . . . . . . . . 11
6		limeq 2211	. . . . . . . . . . 11
7	5, 6	syl 12	. . . . . . . . . 10
8	3, 7	orbi12d 475	. . . . . . . . 9 $\/$ $\/$
9	8	negbid 463	. . . . . . . 8 $\/$ $\/$
10		unieq 1927	. . . . . . . . . . . 12
11		fveq2 2832	. . . . . . . . . . . 12
12	5, 10, 11	3syl 21	. . . . . . . . . . 11
13		fveq1 2831	. . . . . . . . . . 11
14	12, 13	eqtrd 1128	. . . . . . . . . 10
15	14	fveq2d 2836	. . . . . . . . 9
16	15	cleq2d 1112	. . . . . . . 8
17	9, 16	anbi12d 476	. . . . . . 7 $\/$ $/\$ $\/$ $/\$
18		rneq 2555	. . . . . . . . . 10
19	18	unieqd 1929	. . . . . . . . 9
20	19	cleq2d 1112	. . . . . . . 8
21	7, 20	anbi12d 476	. . . . . . 7 $/\$ $/\$
22	4, 17, 21	bi3ord 635	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
23	2, 22	anbi12d 476	. . . . 5 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
24	23	biexdv 936	. . . 4 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
25	24	cbvexv 973	. . 3 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
26	25	biabi 1181	. 2 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
27		df-opab 2098	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
28		df-opab 2098	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
29	26, 27, 28	3eqtr4 1126	1 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 1

wb 127 $\/$ wo 195 $/\$ wa 196 $\/$ w3o 580

wex 678

weq 797

cab 1090

wceq 1091

c0 1707

cop 1810

cuni 1919

copab 2055

wlim 2200

cdm 2410

crn 2411

cfv 2422

This theorem is referenced by: rdgval 2978 rdgzer 2979 rdgsuc 2980 rdglim 2981

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-v 1349 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-pw 1799 df-sn 1811 df-pr 1812 df-op 1815 df-uni 1920 df-tr 2042 df-br 2063 df-opab 2098 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-lim 2204 df-xp 2424 df-cnv 2426 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fv 2438