Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem rdgeq2 2973

Description: Equality theorem for the recursive definition generator.

**Assertion**
Ref	Expression
rdgeq2

**Proof of Theorem rdgeq2**
Step	Hyp	Ref	Expression
1		cleq2 1110	. . . . . . . . . . . 12
2	1	anbi2d 468	. . . . . . . . . . 11 $/\$ $/\$
3		pm4.2i 149	. . . . . . . . . . 11 $\/$ $/\$ $\/$ $/\$
4		pm4.2i 149	. . . . . . . . . . 11 $/\$ $/\$
5	2, 3, 4	bi3ord 635	. . . . . . . . . 10 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
6	5	biopabdv 2102	. . . . . . . . 9 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
7	6	fveq1d 2834	. . . . . . . 8 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
8	7	cleq2d 1112	. . . . . . 7 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
9	8	biraldv 1219	. . . . . 6 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
10	9	anbi2d 468	. . . . 5 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
11	10	birexdv 1220	. . . 4 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
12	11	biabdv 1183	. . 3 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
13	12	unieqd 1929	. 2 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
14		df-rdg 2970	. 2 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
15		df-rdg 2970	. 2 $/\$ $/\$ $\/$ $\/$ $/\$ $\/$ $/\$
16	13, 14, 15	3eqtr4g 1147	1

Colors of variables: wff set class

Syntax hints:

wn 1

wi 2 $\/$ wo 195 $/\$ wa 196 $\/$ w3o 580

cab 1090

wceq 1091

wral 1201

wrex 1202

c0 1707

cuni 1919

copab 2055

con0 2199

wlim 2200

cdm 2410

crn 2411

cres 2412

wfn 2417

cfv 2422

crdg 2969

This theorem is referenced by: rdgzert 2982 oav 3119 seqval 4665

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-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-br 2063 df-opab 2098 df-cnv 2426 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fv 2438 df-rdg 2970