Theorem snssg 4787

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 4786	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
2	1	bicomi 223	. 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵)
3		elex 3492	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
4		imbibi 392	. 2 ⊢ (((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) → (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)))
5	2, 3, 4	mpsyl 68	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  Vcvv 3474   ⊆ wss 3948  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3955  df-ss 3965  df-sn 4629

This theorem is referenced by:  snss  4789  tppreqb  4808  snssi  4811  prssg  4822  snelpwg  5442  relsng  5801  fvimacnvALT  7058  fr3nr  7761  vdwapid1  16912  acsfn  17607  cycsubg2  19125  cycsubg2cl  19126  pgpfac1lem1  19985  pgpfac1lem3a  19987  pgpfac1lem3  19988  pgpfac1lem5  19990  pgpfaclem2  19993  lspsnid  20748  lidldvgen  21093  isneip  22829  elnei  22835  iscnp4  22987  cnpnei  22988  nlly2i  23200  1stckgenlem  23277  flimopn  23699  flimclslem  23708  fclsneii  23741  fcfnei  23759  rrx0el  25139  limcvallem  25612  ellimc2  25618  limcflf  25622  limccnp  25632  limccnp2  25633  limcco  25634  lhop2  25756  plyrem  26042  isppw  26842  lpvtx  28583  h1did  31059  rspsnid  32747  dvdsrspss  32753  unitpidl1  32804  mxidlirred  32850  qsdrngilem  32870  evls1fldgencl  33021  erdszelem8  34475  neibastop2  35549  prnc  37238  proot1mul  42243  uneqsn  43078  mnuprdlem1  43333  islptre  44634  rrxsnicc  45315