Metamath Proof Explorer

Theorem mre1cl

Description: In any Moore collection the base set is closed. (Contributed by Stefan O'Rear, 30-Jan-2015)

Ref Expression
Assertion mre1cl 
|- ( C e. ( Moore ` X ) -> X e. C )

Proof

Step Hyp Ref Expression
1 ismre 
 |-  ( C e. ( Moore ` X ) <-> ( C C_ ~P X /\ X e. C /\ A. s e. ~P C ( s =/= (/) -> |^| s e. C ) ) )
2 1 simp2bi 
 |-  ( C e. ( Moore ` X ) -> X e. C )