Metamath Proof Explorer


Theorem unisucg

Description: A transitive class is equal to the union of its successor, closed form. Combines Theorem 4E of Enderton p. 72 and Exercise 6 of Enderton p. 73. (Contributed by NM, 30-Aug-1993) Generalize from unisuc . (Revised by BJ, 28-Dec-2024)

Ref Expression
Assertion unisucg A V Tr A suc A = A

Proof

Step Hyp Ref Expression
1 ssequn1 A A A A = A
2 1 a1i A V A A A A = A
3 df-tr Tr A A A
4 3 a1i A V Tr A A A
5 unisucs A V suc A = A A
6 5 eqeq1d A V suc A = A A A = A
7 2 4 6 3bitr4d A V Tr A suc A = A