Theorem intminss

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

	Ref	Expression
Hypothesis	intminss.1	|- ( x = A -> ( ph <-> ps ) )
Assertion	intminss	|- ( ( A e. B /\ ps ) -> |^| { x e. B | ph } C_ A )

Proof

Step	Hyp	Ref	Expression
1		intminss.1	|- ( x = A -> ( ph <-> ps ) )
2	1	elrab	|- ( A e. { x e. B | ph } <-> ( A e. B /\ ps ) )
3		intss1	|- ( A e. { x e. B | ph } -> |^| { x e. B | ph } C_ A )
4	2 3	sylbir	|- ( ( A e. B /\ ps ) -> |^| { x e. B | ph } C_ A )