Metamath Proof Explorer


Theorem unisuc

Description: A transitive class is equal to the union of its successor, inference form. 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 e. _V
Assertion unisuc
|- ( Tr A <-> U. suc A = A )

Proof

Step Hyp Ref Expression
1 unisuc.1
 |-  A e. _V
2 unisucg
 |-  ( A e. _V -> ( Tr A <-> U. suc A = A ) )
3 1 2 ax-mp
 |-  ( Tr A <-> U. suc A = A )