Description: Image of a union. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | unima | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 | |
|
2 | simpl | |
|
3 | simpr | |
|
4 | 2 3 | unssd | |
5 | 4 | 3adant1 | |
6 | 1 5 | fvelimabd | |
7 | rexun | |
|
8 | 6 7 | bitrdi | |
9 | fvelimab | |
|
10 | 9 | 3adant3 | |
11 | fvelimab | |
|
12 | 11 | 3adant2 | |
13 | 10 12 | orbi12d | |
14 | 8 13 | bitr4d | |
15 | elun | |
|
16 | 14 15 | bitr4di | |
17 | 16 | eqrdv | |