Theorem sspwimpcfVD 45514

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 45163) 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 45513 is sspwimpcfVD 45514 without virtual deductions and was derived from sspwimpcfVD 45514. 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 3467	. . . . . 6 ⊢ 𝑥 ∈ V
2		idn1 45168	. . . . . . 7 ⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
3		idn1 45168	. . . . . . . 8 ⊢ (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ∈ 𝒫 𝐴   )
4		elpwi 4571	. . . . . . . 8 ⊢ (𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴)
5	3, 4	el1 45222	. . . . . . 7 ⊢ (   𝑥 ∈ 𝒫 𝐴   ▶   𝑥 ⊆ 𝐴   )
6		sstr2 3952	. . . . . . . 8 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵))
7	6	impcom 412	. . . . . . 7 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴) → 𝑥 ⊆ 𝐵)
8	2, 5, 7	el12 45319	. . . . . 6 ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
9		elpwg 4567	. . . . . . 7 ⊢ (𝑥 ∈ V → (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵))
10	9	biimpar 482	. . . . . 6 ⊢ ((𝑥 ∈ V ∧ 𝑥 ⊆ 𝐵) → 𝑥 ∈ 𝒫 𝐵)
11	1, 8, 10	el021old 45295	. . . . 5 ⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵   )
12	11	int2 45200	. . . 4 ⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
13	12	gen11 45210	. . 3 ⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
14		df-ss 3930	. . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵))
15	14	biimpri 231	. . 3 ⊢ (∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵) → 𝒫 𝐴 ⊆ 𝒫 𝐵)
16	13, 15	el1 45222	. 2 ⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
17	16	in1 45165	1 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Syntax hints:   → wi 4  ∀wal 1565   ∈ wcel 2149  Vcvv 3463   ⊆ wss 3913  𝒫 cpw 4564

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-ss 3930  df-pw 4566  df-vd1 45164  df-vhc2 45175

This theorem is referenced by: (None)