Theorem ipodrscl

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

	Ref	Expression
Assertion	ipodrscl	⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset → 𝐴 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		isipodrs	⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset ↔ ( 𝐴 ∈ V ∧ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐴 ( 𝑥 ∪ 𝑦 ) ⊆ 𝑧 ) )
2	1	simp1bi	⊢ ( ( toInc ‘ 𝐴 ) ∈ Dirset → 𝐴 ∈ V )