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	$$⊢\mathrm{Tr}A\leftrightarrow \mathrm{Tr}𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		unipw	$$⊢\bigcup 𝒫A=A$$
2	1	sseq1i	$$⊢\bigcup 𝒫A\subseteq 𝒫A\leftrightarrow A\subseteq 𝒫A$$
3		df-tr	$$⊢\mathrm{Tr}𝒫A\leftrightarrow \bigcup 𝒫A\subseteq 𝒫A$$
4		dftr4	$$⊢\mathrm{Tr}A\leftrightarrow A\subseteq 𝒫A$$
5	2 3 4	3bitr4ri	$$⊢\mathrm{Tr}A\leftrightarrow \mathrm{Tr}𝒫A$$