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		dfss2	|- ( 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 ) )