Theorem mress

Description: A Moore-closed subset is a subset. (Contributed by Stefan O'Rear, 31-Jan-2015)

	Ref	Expression
Assertion	mress	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge S\in C\right)\to S\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		mresspw	$$⊢C\in \mathrm{Moore}\left(X\right)\to C\subseteq 𝒫X$$
2	1	sselda	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge S\in C\right)\to S\in 𝒫X$$
3	2	elpwid	$$⊢\left(C\in \mathrm{Moore}\left(X\right)\wedge S\in C\right)\to S\subseteq X$$