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 e. _V
Assertion	unisuc	|- ( Tr A <-> U. suc A = A )

Proof

Step	Hyp	Ref	Expression
1		unisuc.1	|- A e. _V
2		ssequn1	|- ( U. A C_ A <-> ( U. A u. A ) = A )
3		df-tr	|- ( Tr A <-> U. A C_ A )
4		df-suc	|- suc A = ( A u. { A } )
5	4	unieqi	|- U. suc A = U. ( A u. { A } )
6		uniun	|- U. ( A u. { A } ) = ( U. A u. U. { A } )
7	1	unisn	|- U. { A } = A
8	7	uneq2i	|- ( U. A u. U. { A } ) = ( U. A u. A )
9	5 6 8	3eqtri	|- U. suc A = ( U. A u. A )
10	9	eqeq1i	|- ( U. suc A = A <-> ( U. A u. A ) = A )
11	2 3 10	3bitr4i	|- ( Tr A <-> U. suc A = A )