This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ssel

Description: Membership relationships follow from a subclass relationship. (Contributed by NM, 5-Aug-1993) Avoid ax-12 . (Revised by SN, 27-May-2024)

Ref Expression
Assertion ssel 
|- ( A C_ B -> ( C e. A -> C e. B ) )

Proof

Step Hyp Ref Expression
1 df-ss 
 |-  ( A C_ B <-> A. x ( x e. A -> x e. B ) )
2 id 
 |-  ( ( x e. A -> x e. B ) -> ( x e. A -> x e. B ) )
3 2 anim2d 
 |-  ( ( x e. A -> x e. B ) -> ( ( x = C /\ x e. A ) -> ( x = C /\ x e. B ) ) )
4 3 aleximi 
 |-  ( A. x ( x e. A -> x e. B ) -> ( E. x ( x = C /\ x e. A ) -> E. x ( x = C /\ x e. B ) ) )
5 dfclel 
 |-  ( C e. A <-> E. x ( x = C /\ x e. A ) )
6 dfclel 
 |-  ( C e. B <-> E. x ( x = C /\ x e. B ) )
7 4 5 6 3imtr4g 
 |-  ( A. x ( x e. A -> x e. B ) -> ( C e. A -> C e. B ) )
8 1 7 sylbi 
 |-  ( A C_ B -> ( C e. A -> C e. B ) )