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

Metamath Proof Explorer

Theorem ssmin

Description: Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006)

		Ref	Expression
	Assertion	ssmin	$⊢ A \subseteq ⋂ \{x \| (A \subseteq x \land φ)\}$

Step	Hyp	Ref	Expression
1		ssintab	$⊢ A \subseteq ⋂ \{x \| (A \subseteq x \land φ)\} \leftrightarrow \forall x ((A \subseteq x \land φ) \to A \subseteq x)$
2		simpl	$⊢ (A \subseteq x \land φ) \to A \subseteq x$
3	1 2	mpgbir	$⊢ A \subseteq ⋂ \{x \| (A \subseteq x \land φ)\}$