Theorem mrcssvd

Description: The Moore closure of a set is a subset of the base. Deduction form of mrcssv . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mrcssd.1	|- ( ph -> A e. ( Moore ` X ) )
	mrcssd.2	|- N = ( mrCls ` A )
Assertion	mrcssvd	|- ( ph -> ( N ` B ) C_ X )

Proof

Step	Hyp	Ref	Expression
1		mrcssd.1	|- ( ph -> A e. ( Moore ` X ) )
2		mrcssd.2	|- N = ( mrCls ` A )
3	2	mrcssv	|- ( A e. ( Moore ` X ) -> ( N ` B ) C_ X )
4	1 3	syl	|- ( ph -> ( N ` B ) C_ X )