This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ φ → A ∈ Moore ⁡ X
mrcssidd.2 ⊢ N = mrCls ⁡ A
mrcssidd.3 ⊢ φ → U ⊆ X
Assertion mrcssidd ⊢ φ → U ⊆ N ⁡ U

Proof

Step Hyp Ref Expression
1 mrcssidd.1 ⊢ φ → A ∈ Moore ⁡ X
2 mrcssidd.2 ⊢ N = mrCls ⁡ A
3 mrcssidd.3 ⊢ φ → U ⊆ X
4 2 mrcssid ⊢ A ∈ Moore ⁡ X ∧ U ⊆ X → U ⊆ N ⁡ U
5 1 3 4 syl2anc ⊢ φ → U ⊆ N ⁡ U