Theorem trsspwALT3 45393

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 45392, which is the virtual deduction proof trsspwALT 45391 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 3461	. . . 4 ⊢ 𝑥 ∈ V
3	2	elpw 4562	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
4	1, 3	imbitrrdi 255	. 2 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
5	4	ssrdv 3945	1 ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2145   ⊆ wss 3907  𝒫 cpw 4558  Tr wtr 5212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-v 3459  df-ss 3924  df-pw 4560  df-uni 4869  df-tr 5213

This theorem is referenced by: (None)