Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iuneq12df.1 | |
|
iuneq12df.2 | |
||
iuneq12df.3 | |
||
iuneq12df.4 | |
||
iuneq12df.5 | |
||
Assertion | iuneq12df | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq12df.1 | |
|
2 | iuneq12df.2 | |
|
3 | iuneq12df.3 | |
|
4 | iuneq12df.4 | |
|
5 | iuneq12df.5 | |
|
6 | 5 | eleq2d | |
7 | 1 2 3 4 6 | rexeqbid | |
8 | 7 | alrimiv | |
9 | abbi | |
|
10 | df-iun | |
|
11 | df-iun | |
|
12 | 9 10 11 | 3eqtr4g | |
13 | 8 12 | syl | |