Theorem sspwimpcfVD 44946

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 44594) 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 44945 is sspwimpcfVD 44946 without virtual deductions and was derived from sspwimpcfVD 44946. 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.)

1::	⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
2::	⊢ (   ........... 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ∈ 𝒫 𝐴   )
3:2:	⊢ (   ........... 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ⊆ 𝐴   )
4:3,1:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
5::	⊢ 𝑥 ∈ V
6:4,5:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵    )
7:6:	⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)    )
8:7:	⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
9:8:	⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
qed:9:	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Assertion

Ref	Expression
sspwimpcfVD	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Proof of Theorem sspwimpcfVD

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3483	. . . . . 6 ⊢ 𝑥 ∈ V
2		idn1 44599	. . . . . . 7 ⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
3		idn1 44599	. . . . . . . 8 ⊢ (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ∈ 𝒫 𝐴   )
4		elpwi 4606	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
5	3, 4	el1 44653	. . . . . . 7 ⊢ (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ⊆ 𝐴   )
6		sstr2 3989	. . . . . . . 8 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵))
7	6	impcom 407	. . . . . . 7 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 ⊆ 𝐵)
8	2, 5, 7	el12 44751	. . . . . 6 ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
9		elpwg 4602	. . . . . . 7 ⊢ (𝑥 ∈ V → (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵))
10	9	biimpar 477	. . . . . 6 ⊢ ((𝑥 ∈ V ∧ 𝑥 ⊆ 𝐵) → 𝑥 ∈ 𝒫 𝐵)
11	1, 8, 10	el021old 44726	. . . . 5 ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵   )
12	11	int2 44631	. . . 4 ⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
13	12	gen11 44641	. . 3 ⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
14		df-ss 3967	. . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵))
15	14	biimpri 228	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵)
16	13, 15	el1 44653	. 2 ⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
17	16	in1 44596	1 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2107  Vcvv 3479   ⊆ wss 3950  𝒫 cpw 4599

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-v 3481  df-ss 3967  df-pw 4601  df-vd1 44595  df-vhc2 44606

This theorem is referenced by: (None)