Theorem snelpwiOLD

Description: Obsolete version of snelpwi as of 17-Jan-2025. (Contributed by NM, 28-May-1995) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	snelpwiOLD	$$⊢A\in B\to \left\{A\right\}\in 𝒫B$$

Proof

Step	Hyp	Ref	Expression
1		snssi	$$⊢A\in B\to \left\{A\right\}\subseteq B$$
2		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
3	2	elpw	$$⊢\left\{A\right\}\in 𝒫B\leftrightarrow \left\{A\right\}\subseteq B$$
4	1 3	sylibr	$$⊢A\in B\to \left\{A\right\}\in 𝒫B$$