Theorem sspwimpVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) using conjunction-form virtual hypothesis collections. It was completed manually, but has the potential to be completed automatically by a tools program which would invoke Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimp is sspwimpVD without virtual deductions and was derived from sspwimpVD . (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sspwimpVD	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢x\in \mathrm{V}$$
2	1	vd01	$$⊢\left(\top \to x\in \mathrm{V}\right)$$
3		idn1	$$⊢\left(A\subseteq B\to A\subseteq B\right)$$
4		idn1	$$⊢\left(x\in 𝒫A\to x\in 𝒫A\right)$$
5		elpwi	$$⊢x\in 𝒫A\to x\subseteq A$$
6	4 5	el1	$$⊢\left(x\in 𝒫A\to x\subseteq A\right)$$
7		sstr	$$⊢\left(x\subseteq A\wedge A\subseteq B\right)\to x\subseteq B$$
8	7	ancoms	$$⊢\left(A\subseteq B\wedge x\subseteq A\right)\to x\subseteq B$$
9	3 6 8	el12	$$⊢\left(\left(A\subseteq B,x\in 𝒫A\right)\to x\subseteq B\right)$$
10	2 9	elpwgdedVD	$$⊢\left(\left(\top ,\left(A\subseteq B,x\in 𝒫A\right)\right)\to x\in 𝒫B\right)$$
11	2 9 10	un0.1	$$⊢\left(\left(A\subseteq B,x\in 𝒫A\right)\to x\in 𝒫B\right)$$
12	11	int2	$$⊢\left(A\subseteq B\to \left(x\in 𝒫A\to x\in 𝒫B\right)\right)$$
13	12	gen11	$$⊢\left(A\subseteq B\to \forall x\left(x\in 𝒫A\to x\in 𝒫B\right)\right)$$
14		df-ss	$$⊢𝒫A\subseteq 𝒫B\leftrightarrow \forall x\left(x\in 𝒫A\to x\in 𝒫B\right)$$
15	14	biimpri	$$⊢\forall x\left(x\in 𝒫A\to x\in 𝒫B\right)\to 𝒫A\subseteq 𝒫B$$
16	13 15	el1	$$⊢\left(A\subseteq B\to 𝒫A\subseteq 𝒫B\right)$$
17	16	in1	$$⊢A\subseteq B\to 𝒫A\subseteq 𝒫B$$