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\leftrightarrow \bigcup \mathrm{suc}A=A$$

Proof

Step	Hyp	Ref	Expression
1		unisuc.1	$$⊢A\in \mathrm{V}$$
2		ssequn1	$$⊢\bigcup A\subseteq A\leftrightarrow \bigcup A\cup A=A$$
3		df-tr	$$⊢\mathrm{Tr}A\leftrightarrow \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\leftrightarrow \bigcup A\cup A=A$$
11	2 3 10	3bitr4i	$$⊢\mathrm{Tr}A\leftrightarrow \bigcup \mathrm{suc}A=A$$