# Metamath Proof Explorer

## Theorem snssg

Description: The singleton of an element of a class is a subset of the class (general form of snss ). Theorem 7.4 of Quine p. 49. (Contributed by NM, 22-Jul-2001)

Ref Expression
Assertion snssg ${⊢}{A}\in {V}\to \left({A}\in {B}↔\left\{{A}\right\}\subseteq {B}\right)$

### Proof

Step Hyp Ref Expression
1 velsn ${⊢}{x}\in \left\{{A}\right\}↔{x}={A}$
2 1 imbi1i ${⊢}\left({x}\in \left\{{A}\right\}\to {x}\in {B}\right)↔\left({x}={A}\to {x}\in {B}\right)$
3 2 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{A}\right\}\to {x}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {x}\in {B}\right)$
4 3 a1i ${⊢}{A}\in {V}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{A}\right\}\to {x}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {x}\in {B}\right)\right)$
5 dfss2 ${⊢}\left\{{A}\right\}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{A}\right\}\to {x}\in {B}\right)$
6 5 a1i ${⊢}{A}\in {V}\to \left(\left\{{A}\right\}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left\{{A}\right\}\to {x}\in {B}\right)\right)$
7 clel2g ${⊢}{A}\in {V}\to \left({A}\in {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}={A}\to {x}\in {B}\right)\right)$
8 4 6 7 3bitr4rd ${⊢}{A}\in {V}\to \left({A}\in {B}↔\left\{{A}\right\}\subseteq {B}\right)$