Theorem trsspwALT3 45761

Description: Short predicate calculus proof of the left-to-right implication of dftr4 5218. 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 45760, which is the virtual deduction proof trsspwALT 45759 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
trsspwALT3	⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

Proof of Theorem trsspwALT3

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		trss 5222	. . 3 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
2		vex 3455	. . . 4 ⊢ 𝑥 ∈ V
3	2	elpw 4561	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
4	1, 3	imbitrrdi 255	. 2 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
5	4	ssrdv 3937	1 ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ⊆ wss 3899  𝒫 cpw 4557  Tr wtr 5212

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-v 3453  df-ss 3916  df-pw 4559  df-uni 4868  df-tr 5213

This theorem is used by: (None)