| 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 5266. 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 44839, which is the virtual deduction proof trsspwALT 44838 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 5270 | . . 3 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ⊆ 𝐴)) | |
| 2 | vex 3484 | . . . 4 ⊢ 𝑥 ∈ V | |
| 3 | 2 | elpw 4604 | . . 3 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴) |
| 4 | 1, 3 | imbitrrdi 252 | . 2 ⊢ (Tr 𝐴 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 𝐴)) |
| 5 | 4 | ssrdv 3989 | 1 ⊢ (Tr 𝐴 → 𝐴 ⊆ 𝒫 𝐴) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ⊆ wss 3951 𝒫 cpw 4600 Tr wtr 5259 |
| 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 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 df-v 3482 df-ss 3968 df-pw 4602 df-uni 4908 df-tr 5260 |
| This theorem is referenced by: (None) |
| Copyright terms: Public domain | W3C validator |