Metamath Proof Explorer


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 φ ψ
Assertion intminss A B ψ x B | φ A

Proof

Step Hyp Ref Expression
1 intminss.1 x = A φ ψ
2 1 elrab A x B | φ A B ψ
3 intss1 A x B | φ x B | φ A
4 2 3 sylbir A B ψ x B | φ A