Theorem sbss

Description: Set substitution into the first argument of a subset relation. (Contributed by Rodolfo Medina, 7-Jul-2010) (Proof shortened by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	sbss	$$⊢\left[y/x\right]x\subseteq A\leftrightarrow y\subseteq A$$

Proof

Step	Hyp	Ref	Expression
1		sseq1	$$⊢x=z\to \left(x\subseteq A\leftrightarrow z\subseteq A\right)$$
2		sseq1	$$⊢z=y\to \left(z\subseteq A\leftrightarrow y\subseteq A\right)$$
3	1 2	sbievw2	$$⊢\left[y/x\right]x\subseteq A\leftrightarrow y\subseteq A$$