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

Metamath Proof Explorer

Theorem ssabral

Description: The relation for a subclass of a class abstraction is equivalent to restricted quantification. (Contributed by NM, 6-Sep-2006)

		Ref	Expression
	Assertion	ssabral	$⊢ A \subseteq \{x \| φ\} \leftrightarrow \forall x \in A φ$

Step	Hyp	Ref	Expression
1		ssab	$⊢ A \subseteq \{x \| φ\} \leftrightarrow \forall x (x \in A \to φ)$
2		df-ral	$⊢ \forall x \in A φ \leftrightarrow \forall x (x \in A \to φ)$
3	1 2	bitr4i	$⊢ A \subseteq \{x \| φ\} \leftrightarrow \forall x \in A φ$