Metamath Proof Explorer

Theorem ipodrscl

Description: Direction by inclusion as used here implies sethood. (Contributed by Stefan O'Rear, 2-Apr-2015)

Ref Expression
Assertion ipodrscl 
|- ( ( toInc ` A ) e. Dirset -> A e. _V )

Proof

Step Hyp Ref Expression
1 isipodrs 
 |-  ( ( toInc ` A ) e. Dirset <-> ( A e. _V /\ A =/= (/) /\ A. x e. A A. y e. A E. z e. A ( x u. y ) C_ z ) )
2 1 simp1bi 
 |-  ( ( toInc ` A ) e. Dirset -> A e. _V )