# 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}\in \mathrm{V}$
Assertion unisuc ${⊢}\mathrm{Tr}{A}↔\bigcup \mathrm{suc}{A}={A}$

### Proof

Step Hyp Ref Expression
1 unisuc.1 ${⊢}{A}\in \mathrm{V}$
2 ssequn1 ${⊢}\bigcup {A}\subseteq {A}↔\bigcup {A}\cup {A}={A}$
3 df-tr ${⊢}\mathrm{Tr}{A}↔\bigcup {A}\subseteq {A}$
4 df-suc ${⊢}\mathrm{suc}{A}={A}\cup \left\{{A}\right\}$
5 4 unieqi ${⊢}\bigcup \mathrm{suc}{A}=\bigcup \left({A}\cup \left\{{A}\right\}\right)$
6 uniun ${⊢}\bigcup \left({A}\cup \left\{{A}\right\}\right)=\bigcup {A}\cup \bigcup \left\{{A}\right\}$
7 1 unisn ${⊢}\bigcup \left\{{A}\right\}={A}$
8 7 uneq2i ${⊢}\bigcup {A}\cup \bigcup \left\{{A}\right\}=\bigcup {A}\cup {A}$
9 5 6 8 3eqtri ${⊢}\bigcup \mathrm{suc}{A}=\bigcup {A}\cup {A}$
10 9 eqeq1i ${⊢}\bigcup \mathrm{suc}{A}={A}↔\bigcup {A}\cup {A}={A}$
11 2 3 10 3bitr4i ${⊢}\mathrm{Tr}{A}↔\bigcup \mathrm{suc}{A}={A}$