Metamath Proof Explorer

Theorem ssmin

Description: Subclass of the minimum value of class of supersets. (Contributed by NM, 10-Aug-2006)

Ref Expression
Assertion ssmin A x | A x φ


Step Hyp Ref Expression
1 ssintab A x | A x φ x A x φ A x
2 simpl A x φ A x
3 1 2 mpgbir A x | A x φ