Theorem intmin3

Description: Under subset ordering, the intersection of a class abstraction is less than or equal to any of its members. (Contributed by NM, 3-Jul-2005)

	Ref	Expression
Hypotheses	intmin3.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
	intmin3.3	$$⊢\psi$$
Assertion	intmin3	$$⊢A\in V\to \bigcap \left\{x|\phi \right\}\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		intmin3.2	$$⊢x=A\to \left(\phi \leftrightarrow \psi \right)$$
2		intmin3.3	$$⊢\psi$$
3	1	elabg	$$⊢A\in V\to \left(A\in \left\{x|\phi \right\}\leftrightarrow \psi \right)$$
4	2 3	mpbiri	$$⊢A\in V\to A\in \left\{x|\phi \right\}$$
5		intss1	$$⊢A\in \left\{x|\phi \right\}\to \bigcap \left\{x|\phi \right\}\subseteq A$$
6	4 5	syl	$$⊢A\in V\to \bigcap \left\{x|\phi \right\}\subseteq A$$