Theorem snssg 4731

Description: The singleton formed on a set is included in a class if and only if the set is an element of that class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) (Proof shortened by BJ, 1-Jan-2025.)

Assertion

Ref	Expression
snssg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Proof of Theorem snssg

Step	Hyp	Ref	Expression
1		snssb 4730	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
2	1	bicomi 223	. 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵)
3		elex 3459	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
4		imbibi 392	. 2 ⊢ (((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) → (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)))
5	2, 3, 4	mpsyl 68	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2105  Vcvv 3441   ⊆ wss 3898  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915  df-sn 4574

This theorem is referenced by:  snss  4733  tppreqb  4752  snssi  4755  prssg  4766  snelpwg  5387  relsng  5743  fvimacnvALT  6990  fr3nr  7684  vdwapid1  16773  acsfn  17465  cycsubg2  18925  cycsubg2cl  18926  pgpfac1lem1  19772  pgpfac1lem3a  19774  pgpfac1lem3  19775  pgpfac1lem5  19777  pgpfaclem2  19780  lspsnid  20361  lidldvgen  20632  isneip  22362  elnei  22368  iscnp4  22520  cnpnei  22521  nlly2i  22733  1stckgenlem  22810  flimopn  23232  flimclslem  23241  fclsneii  23274  fcfnei  23292  rrx0el  24668  limcvallem  25141  ellimc2  25147  limcflf  25151  limccnp  25161  limccnp2  25162  limcco  25163  lhop2  25285  plyrem  25571  isppw  26369  lpvtx  27727  h1did  30201  rspsnid  31865  erdszelem8  33459  neibastop2  34646  prnc  36338  proot1mul  41295  uneqsn  41962  mnuprdlem1  42219  islptre  43504  rrxsnicc  44185