Description: The injected slot is an element of the structure with replacement. (Contributed by AV, 10-Nov-2021)
Ref | Expression | ||
---|---|---|---|
Hypotheses | setsidel.s | |
|
setsidel.b | |
||
setsidel.r | |
||
setsnidel.c | |
||
setsnidel.d | |
||
setsnidel.s | |
||
setsnidel.n | |
||
Assertion | setsnidel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | setsidel.s | |
|
2 | setsidel.b | |
|
3 | setsidel.r | |
|
4 | setsnidel.c | |
|
5 | setsnidel.d | |
|
6 | setsnidel.s | |
|
7 | setsnidel.n | |
|
8 | 4 | elexd | |
9 | 7 | necomd | |
10 | eldifsn | |
|
11 | 8 9 10 | sylanbrc | |
12 | opelres | |
|
13 | 5 12 | syl | |
14 | 11 6 13 | mpbir2and | |
15 | elun1 | |
|
16 | 14 15 | syl | |
17 | setsval | |
|
18 | 1 2 17 | syl2anc | |
19 | 3 18 | eqtrid | |
20 | 16 19 | eleqtrrd | |