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

Metamath Proof Explorer

Theorem ssrab2f

Description: Subclass relation for a restricted class. (Contributed by Glauco Siliprandi, 26-Jun-2021)

		Ref	Expression
	Hypothesis	ssrab2f.1	$⊢ \underline{Ⅎ} x A$
	Assertion	ssrab2f	$⊢ \{x \in A \| φ\} \subseteq A$

Step	Hyp	Ref	Expression
1		ssrab2f.1	$⊢ \underline{Ⅎ} x A$
2		nfrab1	$⊢ \underline{Ⅎ} x \{x \in A \| φ\}$
3	2 1	dfss3f	$⊢ \{x \in A \| φ\} \subseteq A \leftrightarrow \forall x \in \{x \in A \| φ\} x \in A$
4		rabidim1	$⊢ x \in \{x \in A \| φ\} \to x \in A$
5	3 4	mprgbir	$⊢ \{x \in A \| φ\} \subseteq A$