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

Metamath Proof Explorer

Theorem ssab

Description: Subclass of a class abstraction. (Contributed by NM, 16-Aug-2006)

		Ref	Expression
	Assertion	ssab	$⊢ A \subseteq \{x \| φ\} \leftrightarrow \forall x (x \in A \to φ)$

Step	Hyp	Ref	Expression
1		abid2	$⊢ \{x \| x \in A\} = A$
2	1	sseq1i	$⊢ \{x \| x \in A\} \subseteq \{x \| φ\} \leftrightarrow A \subseteq \{x \| φ\}$
3		ss2ab	$⊢ \{x \| x \in A\} \subseteq \{x \| φ\} \leftrightarrow \forall x (x \in A \to φ)$
4	2 3	bitr3i	$⊢ A \subseteq \{x \| φ\} \leftrightarrow \forall x (x \in A \to φ)$