Metamath Proof Explorer


Theorem unisucs

Description: The union of the successor of a set is equal to the binary union of that set with its union. (Contributed by NM, 30-Aug-1993) Extract from unisuc . (Revised by BJ, 28-Dec-2024)

Ref Expression
Assertion unisucs A V suc A = A A

Proof

Step Hyp Ref Expression
1 df-suc suc A = A A
2 1 unieqi suc A = A A
3 2 a1i A V suc A = A A
4 uniun A A = A A
5 4 a1i A V A A = A A
6 unisng A V A = A
7 6 uneq2d A V A A = A A
8 3 5 7 3eqtrd A V suc A = A A