Theorem snssg 4728

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  Vcvv 3430   ⊆ wss 3890  {csn 4568

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-sn 4569

This theorem is referenced by:  snss  4729  tppreqb  4749  snssi  4752  prssg  4763  snelpwg  5390  relsng  5750  fvimacnvALT  7003  fr3nr  7719  vdwapid1  16937  acsfn  17616  cycsubg2  19176  cycsubg2cl  19177  pgpfac1lem1  20042  pgpfac1lem3a  20044  pgpfac1lem3  20045  pgpfac1lem5  20047  pgpfaclem2  20050  lspsnid  20979  lidldvgen  21324  isneip  23080  elnei  23086  iscnp4  23238  cnpnei  23239  nlly2i  23451  1stckgenlem  23528  flimopn  23950  flimclslem  23959  fclsneii  23992  fcfnei  24010  rrx0el  25375  limcvallem  25848  ellimc2  25854  limcflf  25858  limccnp  25868  limccnp2  25869  limcco  25870  lhop2  25992  plyrem  26282  isppw  27091  lpvtx  29151  h1did  31637  prssad  32614  prssbd  32615  tpssg  32622  rspsnid  33446  dvdsrspss  33462  unitpidl1  33499  mxidlirred  33547  qsdrngilem  33569  evls1fldgencl  33830  erdszelem8  35396  neibastop2  36559  prnc  38402  proot1mul  43640  uneqsn  44470  mnuprdlem1  44717  islptre  46067  rrxsnicc  46746  sclnbgrelself  48336