Description: Preimage maps produced by the membership relation. (Contributed by Thierry Arnoux, 6-Feb-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | dstrvprob.1 | |
|
dstrvprob.2 | |
||
orvcelel.1 | |
||
Assertion | orvcelval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dstrvprob.1 | |
|
2 | dstrvprob.2 | |
|
3 | orvcelel.1 | |
|
4 | 1 2 3 | orrvcval4 | |
5 | epelg | |
|
6 | 3 5 | syl | |
7 | 6 | rabbidv | |
8 | dfin5 | |
|
9 | 8 | a1i | |
10 | elssuni | |
|
11 | unibrsiga | |
|
12 | 10 11 | sseqtrdi | |
13 | 3 12 | syl | |
14 | sseqin2 | |
|
15 | 13 14 | sylib | |
16 | 7 9 15 | 3eqtr2d | |
17 | 16 | imaeq2d | |
18 | 4 17 | eqtrd | |