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 C_ |^| { x | ( A C_ x /\ ph ) }

Proof

Step Hyp Ref Expression
1 ssintab 
 |-  ( A C_ |^| { x | ( A C_ x /\ ph ) } <-> A. x ( ( A C_ x /\ ph ) -> A C_ x ) )
2 simpl 
 |-  ( ( A C_ x /\ ph ) -> A C_ x )
3 1 2 mpgbir 
 |-  A C_ |^| { x | ( A C_ x /\ ph ) }