Description: Show closure of the unique element in cdleme29c . (Contributed by NM, 27-Mar-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | cdlemefs32.b | |
|
cdlemefs32.l | |
||
cdlemefs32.j | |
||
cdlemefs32.m | |
||
cdlemefs32.a | |
||
cdlemefs32.h | |
||
cdlemefs32.u | |
||
cdlemefs32.d | |
||
cdlemefs32.e | |
||
cdlemefs32.i | |
||
cdlemefs32.n | |
||
cdlemefs29cl.o | |
||
Assertion | cdlemefs29clN | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemefs32.b | |
|
2 | cdlemefs32.l | |
|
3 | cdlemefs32.j | |
|
4 | cdlemefs32.m | |
|
5 | cdlemefs32.a | |
|
6 | cdlemefs32.h | |
|
7 | cdlemefs32.u | |
|
8 | cdlemefs32.d | |
|
9 | cdlemefs32.e | |
|
10 | cdlemefs32.i | |
|
11 | cdlemefs32.n | |
|
12 | cdlemefs29cl.o | |
|
13 | breq1 | |
|
14 | simp1 | |
|
15 | simp3l | |
|
16 | simp3rl | |
|
17 | 15 16 | jca | |
18 | simp3rr | |
|
19 | simp2 | |
|
20 | 1 2 3 4 5 6 7 8 9 10 11 | cdlemefs27cl | |
21 | 14 17 18 19 20 | syl13anc | |
22 | 1 2 3 4 5 6 7 8 9 10 11 | cdlemefs32snb | |
23 | 1 2 3 4 5 6 13 21 22 12 | cdlemefrs29clN | |