Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > sspwimpcfVD | Structured version Visualization version GIF version |
Description: The following User's Proof is a Virtual Deduction proof (see wvd1 37806)
using conjunction-form virtual hypothesis collections. It was completed
automatically by a tools program which would invokes Mel L. O'Cat's mmj2
and Norm Megill's Metamath Proof Assistant.
sspwimpcf 38178 is sspwimpcfVD 38179 without virtual deductions and was derived
from sspwimpcfVD 38179.
The version of completeusersproof.cmd used is capable of only generating
conjunction-form unification theorems, not unification deductions.
(Contributed by Alan Sare, 13-Jun-2015.)
(Proof modification is discouraged.) (New usage is discouraged.)
|
Ref | Expression |
---|---|
sspwimpcfVD | ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3176 | . . . . . 6 ⊢ 𝑥 ∈ V | |
2 | idn1 37811 | . . . . . . 7 ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝐴 ⊆ 𝐵 ) | |
3 | idn1 37811 | . . . . . . . 8 ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ∈ 𝒫 𝐴 ) | |
4 | elpwi 4117 | . . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴) | |
5 | 3, 4 | el1 37874 | . . . . . . 7 ⊢ ( 𝑥 ∈ 𝒫 𝐴 ▶ 𝑥 ⊆ 𝐴 ) |
6 | sstr2 3575 | . . . . . . . 8 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵)) | |
7 | 6 | impcom 445 | . . . . . . 7 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 ⊆ 𝐵) |
8 | 2, 5, 7 | el12 37974 | . . . . . 6 ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ⊆ 𝐵 ) |
9 | elpwg 4116 | . . . . . . 7 ⊢ (𝑥 ∈ V → (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)) | |
10 | 9 | biimpar 501 | . . . . . 6 ⊢ ((𝑥 ∈ V ∧ 𝑥 ⊆ 𝐵) → 𝑥 ∈ 𝒫 𝐵) |
11 | 1, 8, 10 | el021old 37947 | . . . . 5 ⊢ ( ( 𝐴 ⊆ 𝐵 , 𝑥 ∈ 𝒫 𝐴 ) ▶ 𝑥 ∈ 𝒫 𝐵 ) |
12 | 11 | int2 37852 | . . . 4 ⊢ ( 𝐴 ⊆ 𝐵 ▶ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) ) |
13 | 12 | gen11 37862 | . . 3 ⊢ ( 𝐴 ⊆ 𝐵 ▶ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) ) |
14 | dfss2 3557 | . . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)) | |
15 | 14 | biimpri 217 | . . 3 ⊢ (∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
16 | 13, 15 | el1 37874 | . 2 ⊢ ( 𝐴 ⊆ 𝐵 ▶ 𝒫 𝐴 ⊆ 𝒫 𝐵 ) |
17 | 16 | in1 37808 | 1 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1473 ∈ wcel 1977 Vcvv 3173 ⊆ wss 3540 𝒫 cpw 4108 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-in 3547 df-ss 3554 df-pw 4110 df-vd1 37807 df-vhc2 37818 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |