Metamath Proof Explorer
Description: Equality deduction for indexed union. (Contributed by Giovanni
Mascellani, 9-Apr-2018)
|
|
Ref |
Expression |
|
Hypotheses |
iuneq2f.1 |
|
|
|
iuneq2f.2 |
|
|
Assertion |
iuneq2f |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
iuneq2f.1 |
|
2 |
|
iuneq2f.2 |
|
3 |
1 2
|
nfeq |
|
4 |
|
id |
|
5 |
|
eqidd |
|
6 |
3 1 2 4 5
|
iuneq12df |
|