Theorem trsspwALT3 44813

Description: Short predicate calculus proof of the left-to-right implication of dftr4 5205. 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 44812, which is the virtual deduction proof trsspwALT 44811 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 5209	. . 3 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
2		vex 3440	. . . 4 ⊢ 𝑥 ∈ V
3	2	elpw 4555	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
4	1, 3	imbitrrdi 252	. 2 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
5	4	ssrdv 3941	1 ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3903  𝒫 cpw 4551  Tr wtr 5199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-v 3438  df-ss 3920  df-pw 4553  df-uni 4859  df-tr 5200

This theorem is referenced by: (None)