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

Metamath Proof Explorer

Theorem snss

Description: The singleton of an element of a class is a subset of the class (inference form of snssg ). Theorem 7.4 of Quine p. 49. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis snss.1 ⊢ A ∈ V
Assertion snss ⊢ A ∈ B ↔ A ⊆ B

Proof

Step Hyp Ref Expression
1 snss.1 ⊢ A ∈ V
2 snssg ⊢ A ∈ V → A ∈ B ↔ A ⊆ B
3 1 2 ax-mp ⊢ A ∈ B ↔ A ⊆ B