Theorem pwtr

Description: A class is transitive iff its power class is transitive. (Contributed by Alan Sare, 25-Aug-2011) (Revised by Mario Carneiro, 15-Jun-2014)

	Ref	Expression
Assertion	pwtr	|- ( Tr A <-> Tr ~P A )

Proof

Step	Hyp	Ref	Expression
1		unipw	|- U. ~P A = A
2	1	sseq1i	|- ( U. ~P A C_ ~P A <-> A C_ ~P A )
3		df-tr	|- ( Tr ~P A <-> U. ~P A C_ ~P A )
4		dftr4	|- ( Tr A <-> A C_ ~P A )
5	2 3 4	3bitr4ri	|- ( Tr A <-> Tr ~P A )