Metamath Proof Explorer


Theorem iunp1

Description: The addition of the next set to a union indexed by a finite set of sequential integers. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses iunp1.1 _ k B
iunp1.2 φ N M
iunp1.3 k = N + 1 A = B
Assertion iunp1 φ k = M N + 1 A = k = M N A B

Proof

Step Hyp Ref Expression
1 iunp1.1 _ k B
2 iunp1.2 φ N M
3 iunp1.3 k = N + 1 A = B
4 fzsuc N M M N + 1 = M N N + 1
5 2 4 syl φ M N + 1 = M N N + 1
6 5 iuneq1d φ k = M N + 1 A = k M N N + 1 A
7 iunxun k M N N + 1 A = k = M N A k N + 1 A
8 7 a1i φ k M N N + 1 A = k = M N A k N + 1 A
9 ovex N + 1 V
10 1 9 3 iunxsnf k N + 1 A = B
11 10 a1i φ k N + 1 A = B
12 11 uneq2d φ k = M N A k N + 1 A = k = M N A B
13 6 8 12 3eqtrd φ k = M N + 1 A = k = M N A B