Theorem trsspwALT3 43340

Description: Short predicate calculus proof of the left-to-right implication of dftr4 5264. 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 43339, which is the virtual deduction proof trsspwALT 43338 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 5268	. . 3 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
2		vex 3476	. . . 4 ⊢ 𝑥 ∈ V
3	2	elpw 4599	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
4	1, 3	syl6ibr 251	. 2 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
5	4	ssrdv 3983	1 ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3943  𝒫 cpw 4595  Tr wtr 5257

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-v 3474  df-in 3950  df-ss 3960  df-pw 4597  df-uni 4901  df-tr 5258

This theorem is referenced by: (None)