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

Metamath Proof Explorer

Theorem intmin2

Description: Any set is the smallest of all sets that include it. (Contributed by NM, 20-Sep-2003)

		Ref	Expression
	Hypothesis	intmin2.1	$⊢ A \in V$
	Assertion	intmin2	$⊢ ⋂ \{x \| A \subseteq x\} = A$

Step	Hyp	Ref	Expression
1		intmin2.1	$⊢ A \in V$
2		rabab	$⊢ \{x \in V \| A \subseteq x\} = \{x \| A \subseteq x\}$
3	2	inteqi	$⊢ ⋂ \{x \in V \| A \subseteq x\} = ⋂ \{x \| A \subseteq x\}$
4		intmin	$⊢ A \in V \to ⋂ \{x \in V \| A \subseteq x\} = A$
5	1 4	ax-mp	$⊢ ⋂ \{x \in V \| A \subseteq x\} = A$
6	3 5	eqtr3i	$⊢ ⋂ \{x \| A \subseteq x\} = A$