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\subseteq B\to \left(C\in A\to C\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-ss	$$⊢A\subseteq B\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$
2		id	$$⊢\left(x\in A\to x\in B\right)\to \left(x\in A\to x\in B\right)$$
3	2	anim2d	$$⊢\left(x\in A\to x\in B\right)\to \left(\left(x=C\wedge x\in A\right)\to \left(x=C\wedge x\in B\right)\right)$$
4	3	aleximi	$$⊢\forall x\left(x\in A\to x\in B\right)\to \left(\exists x\left(x=C\wedge x\in A\right)\to \exists x\left(x=C\wedge x\in B\right)\right)$$
5		dfclel	$$⊢C\in A\leftrightarrow \exists x\left(x=C\wedge x\in A\right)$$
6		dfclel	$$⊢C\in B\leftrightarrow \exists x\left(x=C\wedge x\in B\right)$$
7	4 5 6	3imtr4g	$$⊢\forall x\left(x\in A\to x\in B\right)\to \left(C\in A\to C\in B\right)$$
8	1 7	sylbi	$$⊢A\subseteq B\to \left(C\in A\to C\in B\right)$$