Theorem sspwimpcfVD 44953

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 44602) 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 44952 is sspwimpcfVD 44953 without virtual deductions and was derived from sspwimpcfVD 44953. 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 3440	. . . . . 6 ⊢ 𝑥 ∈ V
2		idn1 44607	. . . . . . 7 ⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
3		idn1 44607	. . . . . . . 8 ⊢ (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ∈ 𝒫 𝐴   )
4		elpwi 4552	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
5	3, 4	el1 44661	. . . . . . 7 ⊢ (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ⊆ 𝐴   )
6		sstr2 3936	. . . . . . . 8 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵))
7	6	impcom 407	. . . . . . 7 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 ⊆ 𝐵)
8	2, 5, 7	el12 44758	. . . . . 6 ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
9		elpwg 4548	. . . . . . 7 ⊢ (𝑥 ∈ V → (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵))
10	9	biimpar 477	. . . . . 6 ⊢ ((𝑥 ∈ V ∧ 𝑥 ⊆ 𝐵) → 𝑥 ∈ 𝒫 𝐵)
11	1, 8, 10	el021old 44734	. . . . 5 ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵   )
12	11	int2 44639	. . . 4 ⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
13	12	gen11 44649	. . 3 ⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
14		df-ss 3914	. . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵))
15	14	biimpri 228	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵)
16	13, 15	el1 44661	. 2 ⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
17	16	in1 44604	1 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3897  𝒫 cpw 4545

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3914  df-pw 4547  df-vd1 44603  df-vhc2 44614

This theorem is referenced by: (None)