Theorem snssg 4754

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 4753	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
2	1	bicomi 227	. 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵)
3		elex 3479	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
4		imbibi 396	. 2 ⊢ (((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) → (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)))
5	2, 3, 4	mpsyl 69	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2146  Vcvv 3458   ⊆ wss 3908  {csn 4594

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-ss 3925  df-sn 4595

This theorem is used by:  snss  4755  snssi  4756  tppreqb  4778  prssg  4790  snelpwg  5429  relsng  5793  fvimacnvALT  7059  fr3nr  7780  sucprcreg  9578  vdwapid1  17060  acsfn  17740  cycsubg2  19312  cycsubg2cl  19313  pgpfac1lem1  20177  pgpfac1lem3a  20179  pgpfac1lem3  20180  pgpfac1lem5  20182  pgpfaclem2  20185  lspsnid  21151  rspsnid  21410  lidldvgen  21539  isneip  23299  elnei  23305  iscnp4  23457  cnpnei  23458  nlly2i  23670  1stckgenlem  23747  flimopn  24169  flimclslem  24178  fclsneii  24211  fcfnei  24229  rrx0el  25594  limcvallem  26067  ellimc2  26073  limcflf  26077  limccnp  26087  limccnp2  26088  limcco  26089  lhop2  26211  plyrem  26503  isppw  27315  lpvtx  29455  h1did  31940  prssad  32912  prssbd  32913  tpssg  32920  dvdsrspss  33731  unitpidl1  33763  mxidlirred  33786  qsdrngilem  33807  evls1fldgencl  34091  erdszelem8  35711  neibastop2  36913  prnc  38759  proot1mul  43962  uneqsn  44792  mnuprdlem1  45023  islptre  46376  rrxsnicc  47055  sclnbgrelself  48654