Theorem snssg 4745

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2145  Vcvv 3457   ⊆ wss 3907  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-ss 3924  df-sn 4586

This theorem is referenced by:  snss  4746  snssi  4747  tppreqb  4768  prssg  4780  snelpwg  5414  relsng  5778  fvimacnvALT  7042  fr3nr  7759  sucprcreg  9556  vdwapid1  17023  acsfn  17703  cycsubg2  19269  cycsubg2cl  19270  pgpfac1lem1  20134  pgpfac1lem3a  20136  pgpfac1lem3  20137  pgpfac1lem5  20139  pgpfaclem2  20142  lspsnid  21080  rspsnid  21336  lidldvgen  21459  isneip  23219  elnei  23225  iscnp4  23377  cnpnei  23378  nlly2i  23590  1stckgenlem  23667  flimopn  24089  flimclslem  24098  fclsneii  24131  fcfnei  24149  rrx0el  25514  limcvallem  25987  ellimc2  25993  limcflf  25997  limccnp  26007  limccnp2  26008  limcco  26009  lhop2  26131  plyrem  26423  isppw  27232  lpvtx  29323  h1did  31808  prssad  32781  prssbd  32782  tpssg  32789  dvdsrspss  33611  unitpidl1  33643  mxidlirred  33667  qsdrngilem  33688  evls1fldgencl  33972  erdszelem8  35556  neibastop2  36729  prnc  38573  proot1mul  43778  uneqsn  44608  mnuprdlem1  44841  islptre  46194  rrxsnicc  46873  sclnbgrelself  48469