Theorem snssiALTVD

Description: Virtual deduction proof of snssiALT . (Contributed by Alan Sare, 11-Sep-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	snssiALTVD	$$⊢A\in B\to \left\{A\right\}\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		dfss2	$$⊢\left\{A\right\}\subseteq B\leftrightarrow \forall x\left(x\in \left\{A\right\}\to x\in B\right)$$
2		idn1	$$⊢\left(A\in B\to A\in B\right)$$
3		idn2	$$⊢\left(A\in B,x\in \left\{A\right\}\to x\in \left\{A\right\}\right)$$
4		velsn	$$⊢x\in \left\{A\right\}\leftrightarrow x=A$$
5	3 4	e2bi	$$⊢\left(A\in B,x\in \left\{A\right\}\to x=A\right)$$
6		eleq1a	$$⊢A\in B\to \left(x=A\to x\in B\right)$$
7	2 5 6	e12	$$⊢\left(A\in B,x\in \left\{A\right\}\to x\in B\right)$$
8	7	in2	$$⊢\left(A\in B\to \left(x\in \left\{A\right\}\to x\in B\right)\right)$$
9	8	gen11	$$⊢\left(A\in B\to \forall x\left(x\in \left\{A\right\}\to x\in B\right)\right)$$
10		biimpr	$$⊢\left(\left\{A\right\}\subseteq B\leftrightarrow \forall x\left(x\in \left\{A\right\}\to x\in B\right)\right)\to \left(\forall x\left(x\in \left\{A\right\}\to x\in B\right)\to \left\{A\right\}\subseteq B\right)$$
11	1 9 10	e01	$$⊢\left(A\in B\to \left\{A\right\}\subseteq B\right)$$
12	11	in1	$$⊢A\in B\to \left\{A\right\}\subseteq B$$