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	⊢ ( Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		trss	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴 ) )
2		vex	⊢ 𝑥 ∈ V
3	2	elpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
4	1 3	syl6ibr	⊢ ( Tr 𝐴 → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
5	4	ssrdv	⊢ ( Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴 )