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 -> ( ph <-> ps ) )
	intmin3.3	|- ps
Assertion	intmin3	|- ( A e. V -> |^| { x | ph } C_ A )

Proof

Step	Hyp	Ref	Expression
1		intmin3.2	|- ( x = A -> ( ph <-> ps ) )
2		intmin3.3	|- ps
3	1	elabg	|- ( A e. V -> ( A e. { x | ph } <-> ps ) )
4	2 3	mpbiri	|- ( A e. V -> A e. { x | ph } )
5		intss1	|- ( A e. { x | ph } -> |^| { x | ph } C_ A )
6	4 5	syl	|- ( A e. V -> |^| { x | ph } C_ A )