Metamath Proof Explorer


Theorem unisuc

Description: A transitive class is equal to the union of its successor. Combines Theorem 4E of Enderton p. 72 and Exercise 6 of Enderton p. 73. (Contributed by NM, 30-Aug-1993)

Ref Expression
Hypothesis unisuc.1 A V
Assertion unisuc Tr A suc A = A

Proof

Step Hyp Ref Expression
1 unisuc.1 A V
2 ssequn1 A A A A = A
3 df-tr Tr A A A
4 df-suc suc A = A A
5 4 unieqi suc A = A A
6 uniun A A = A A
7 1 unisn A = A
8 7 uneq2i A A = A A
9 5 6 8 3eqtri suc A = A A
10 9 eqeq1i suc A = A A A = A
11 2 3 10 3bitr4i Tr A suc A = A