![]() |
Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > trsspwALT3 | Structured version Visualization version GIF version |
Description: Short predicate calculus proof of the left-to-right implication of dftr4 5265. 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 44156, which is the virtual deduction proof trsspwALT 44155 without virtual deductions. (Contributed by Alan Sare, 30-Apr-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
trsspwALT3 | ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | trss 5269 | . . 3 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) | |
2 | vex 3472 | . . . 4 ⊢ 𝑥 ∈ V | |
3 | 2 | elpw 4601 | . . 3 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
4 | 1, 3 | imbitrrdi 251 | . 2 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴)) |
5 | 4 | ssrdv 3983 | 1 ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2098 ⊆ wss 3943 𝒫 cpw 4597 Tr wtr 5258 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2704 df-cleq 2718 df-clel 2804 df-ral 3056 df-v 3470 df-in 3950 df-ss 3960 df-pw 4599 df-uni 4903 df-tr 5259 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |