Theorem sselOLD

Description: Obsolete version of ssel as of 27-May-2024. (Contributed by NM, 5-Aug-1993) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sselOLD	$$⊢A\subseteq B\to \left(C\in A\to C\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfss2	$$⊢A\subseteq B\leftrightarrow \forall x\left(x\in A\to x\in B\right)$$
2	1	biimpi	$$⊢A\subseteq B\to \forall x\left(x\in A\to x\in B\right)$$
3	2	19.21bi	$$⊢A\subseteq B\to \left(x\in A\to x\in B\right)$$
4	3	anim2d	$$⊢A\subseteq B\to \left(\left(x=C\wedge x\in A\right)\to \left(x=C\wedge x\in B\right)\right)$$
5	4	eximdv	$$⊢A\subseteq B\to \left(\exists x\left(x=C\wedge x\in A\right)\to \exists x\left(x=C\wedge x\in B\right)\right)$$
6		dfclel	$$⊢C\in A\leftrightarrow \exists x\left(x=C\wedge x\in A\right)$$
7		dfclel	$$⊢C\in B\leftrightarrow \exists x\left(x=C\wedge x\in B\right)$$
8	5 6 7	3imtr4g	$$⊢A\subseteq B\to \left(C\in A\to C\in B\right)$$