ssextss

Description: An extensionality-like principle defining subclass in terms of subsets. (Contributed by NM, 30-Jun-2004)

		Ref	Expression
	Assertion	ssextss	$⊢ A \subseteq B \leftrightarrow \forall x (x \subseteq A \to x \subseteq B)$

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

Metamath Proof Explorer