Description: Any particular operator value is the subset of the index union over a set of operator values. Generalized from rtrclreclem1 and rtrclreclem2 . (Contributed by RP, 4-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ov2ssiunov2.def | |
|
Assertion | ov2ssiunov2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ov2ssiunov2.def | |
|
2 | simp3 | |
|
3 | simpr | |
|
4 | 3 | oveq2d | |
5 | 4 | eleq2d | |
6 | 2 5 | rspcedv | |
7 | 1 | eliunov2 | |
8 | 7 | biimprd | |
9 | 8 | 3adant3 | |
10 | 6 9 | syld | |
11 | 10 | ssrdv | |