This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V
Assertion unisuc ⊢ Tr ⁡ A ↔ ⋃ suc ⁡ A = A

Proof

Step Hyp Ref Expression
1 unisuc.1 ⊢ A ∈ V
2 unisucg ⊢ A ∈ V → Tr ⁡ A ↔ ⋃ suc ⁡ A = A
3 1 2 ax-mp ⊢ Tr ⁡ A ↔ ⋃ suc ⁡ A = A