This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem pwss

Description: Subclass relationship for power class. (Contributed by NM, 21-Jun-2009)

		Ref	Expression
	Assertion	pwss	$⊢ 𝒫 A \subseteq B \leftrightarrow \forall x (x \subseteq A \to x \in B)$

Step	Hyp	Ref	Expression
1		df-ss	$⊢ 𝒫 A \subseteq B \leftrightarrow \forall x (x \in 𝒫 A \to x \in B)$
2		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
3	2	imbi1i	$⊢ (x \in 𝒫 A \to x \in B) \leftrightarrow (x \subseteq A \to x \in B)$
4	3	albii	$⊢ \forall x (x \in 𝒫 A \to x \in B) \leftrightarrow \forall x (x \subseteq A \to x \in B)$
5	1 4	bitri	$⊢ 𝒫 A \subseteq B \leftrightarrow \forall x (x \subseteq A \to x \in B)$