Theorem mrcssidd

Description: A set is contained in its Moore closure. Deduction form of mrcssid . (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Hypotheses	mrcssidd.1	|- ( ph -> A e. ( Moore ` X ) )
	mrcssidd.2	|- N = ( mrCls ` A )
	mrcssidd.3	|- ( ph -> U C_ X )
Assertion	mrcssidd	|- ( ph -> U C_ ( N ` U ) )

Proof

Step	Hyp	Ref	Expression
1		mrcssidd.1	|- ( ph -> A e. ( Moore ` X ) )
2		mrcssidd.2	|- N = ( mrCls ` A )
3		mrcssidd.3	|- ( ph -> U C_ X )
4	2	mrcssid	|- ( ( A e. ( Moore ` X ) /\ U C_ X ) -> U C_ ( N ` U ) )
5	1 3 4	syl2anc	|- ( ph -> U C_ ( N ` U ) )