Metamath Proof Explorer

Theorem sselda

Description: Membership deduction from subclass relationship. (Contributed by NM, 26-Jun-2014)

Ref Expression
Hypothesis sseld.1 
|- ( ph -> A C_ B )
Assertion sselda 
|- ( ( ph /\ C e. A ) -> C e. B )

Proof

Step Hyp Ref Expression
1 sseld.1 
 |-  ( ph -> A C_ B )
2 1 sseld 
 |-  ( ph -> ( C e. A -> C e. B ) )
3 2 imp 
 |-  ( ( ph /\ C e. A ) -> C e. B )