Theorem trsspwALT3 45895

Description: Short predicate calculus proof of the left-to-right implication of dftr4 5217. 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 45894, which is the virtual deduction proof trsspwALT 45893 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 5221	. . 3 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴))
2		vex 3454	. . . 4 ⊢ 𝑥 ∈ V
3	2	elpw 4560	. . 3 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
4	1, 3	imbitrrdi 255	. 2 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴))
5	4	ssrdv 3914	1 ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ⊆ wss 3895  𝒫 cpw 4556  Tr wtr 5211

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-v 3452  df-ss 3896  df-pw 4558  df-uni 4867  df-tr 5212

This theorem is used by: (None)