Theorem snwf

Description: A singleton is well-founded if its element is. (Contributed by Mario Carneiro, 10-Jun-2013) (Revised by Mario Carneiro, 16-Nov-2014)

	Ref	Expression
Assertion	snwf	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \left\{A\right\}\in \bigcup R_1\left[\mathrm{On}\right]$$

Proof

Step	Hyp	Ref	Expression
1		pwwf	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\leftrightarrow 𝒫A\in \bigcup R_1\left[\mathrm{On}\right]$$
2		snsspw	$$⊢\left\{A\right\}\subseteq 𝒫A$$
3		sswf	$$⊢\left(𝒫A\in \bigcup R_1\left[\mathrm{On}\right]\wedge \left\{A\right\}\subseteq 𝒫A\right)\to \left\{A\right\}\in \bigcup R_1\left[\mathrm{On}\right]$$
4	2 3	mpan2	$$⊢𝒫A\in \bigcup R_1\left[\mathrm{On}\right]\to \left\{A\right\}\in \bigcup R_1\left[\mathrm{On}\right]$$
5	1 4	sylbi	$$⊢A\in \bigcup R_1\left[\mathrm{On}\right]\to \left\{A\right\}\in \bigcup R_1\left[\mathrm{On}\right]$$