Theorem trsspwALT3

Description: Short predicate calculus proof of the left-to-right implication of dftr4 . A transitive class is a subset of its power class. This proof was constructed by applying Metamath's minimize command to the proof of trsspwALT2 , which is the virtual deduction proof trsspwALT without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	trsspwALT3	$$⊢\mathrm{Tr}A\to A\subseteq 𝒫A$$

Proof

Step	Hyp	Ref	Expression
1		trss	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\subseteq A\right)$$
2		vex	$$⊢x\in \mathrm{V}$$
3	2	elpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
4	1 3	imbitrrdi	$$⊢\mathrm{Tr}A\to \left(x\in A\to x\in 𝒫A\right)$$
5	4	ssrdv	$$⊢\mathrm{Tr}A\to A\subseteq 𝒫A$$