Metamath Proof Explorer

Theorem mress

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

Ref Expression
Assertion mress 
|- ( ( C e. ( Moore ` X ) /\ S e. C ) -> S C_ X )

Proof

Step Hyp Ref Expression
1 mresspw 
 |-  ( C e. ( Moore ` X ) -> C C_ ~P X )
2 1 sselda 
 |-  ( ( C e. ( Moore ` X ) /\ S e. C ) -> S e. ~P X )
3 2 elpwid 
 |-  ( ( C e. ( Moore ` X ) /\ S e. C ) -> S C_ X )