Theorem snssg 4742

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  Vcvv 3442   ⊆ wss 3903  {csn 4582

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 3444  df-ss 3920  df-sn 4583

This theorem is referenced by:  snss  4743  tppreqb  4763  snssi  4766  prssg  4777  snelpwg  5398  relsng  5758  fvimacnvALT  7011  fr3nr  7727  vdwapid1  16915  acsfn  17594  cycsubg2  19151  cycsubg2cl  19152  pgpfac1lem1  20017  pgpfac1lem3a  20019  pgpfac1lem3  20020  pgpfac1lem5  20022  pgpfaclem2  20025  lspsnid  20956  lidldvgen  21301  isneip  23061  elnei  23067  iscnp4  23219  cnpnei  23220  nlly2i  23432  1stckgenlem  23509  flimopn  23931  flimclslem  23940  fclsneii  23973  fcfnei  23991  rrx0el  25366  limcvallem  25840  ellimc2  25846  limcflf  25850  limccnp  25860  limccnp2  25861  limcco  25862  lhop2  25988  plyrem  26281  isppw  27092  lpvtx  29153  h1did  31638  prssad  32615  prssbd  32616  tpssg  32623  rspsnid  33463  dvdsrspss  33479  unitpidl1  33516  mxidlirred  33564  qsdrngilem  33586  evls1fldgencl  33847  erdszelem8  35411  neibastop2  36574  prnc  38315  proot1mul  43548  uneqsn  44378  mnuprdlem1  44625  islptre  45976  rrxsnicc  46655  sclnbgrelself  48205