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

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 ∈ Dirset → A ∈ V

Proof

Step Hyp Ref Expression
1 isipodrs ⊢ toInc ⁡ A ∈ Dirset ↔ A ∈ V ∧ A ≠ ∅ ∧ ∀ x ∈ A ∀ y ∈ A ∃ z ∈ A x ∪ y ⊆ z
2 1 simp1bi ⊢ toInc ⁡ A ∈ Dirset → A ∈ V