Theorem snssg 4786

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  Vcvv 3475   ⊆ wss 3947  {csn 4627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3954  df-ss 3964  df-sn 4628

This theorem is referenced by:  snss  4788  tppreqb  4807  snssi  4810  prssg  4821  snelpwg  5441  relsng  5799  fvimacnvALT  7054  fr3nr  7754  vdwapid1  16904  acsfn  17599  cycsubg2  19081  cycsubg2cl  19082  pgpfac1lem1  19936  pgpfac1lem3a  19938  pgpfac1lem3  19939  pgpfac1lem5  19941  pgpfaclem2  19944  lspsnid  20592  lidldvgen  20880  isneip  22591  elnei  22597  iscnp4  22749  cnpnei  22750  nlly2i  22962  1stckgenlem  23039  flimopn  23461  flimclslem  23470  fclsneii  23503  fcfnei  23521  rrx0el  24897  limcvallem  25370  ellimc2  25376  limcflf  25380  limccnp  25390  limccnp2  25391  limcco  25392  lhop2  25514  plyrem  25800  isppw  26598  lpvtx  28308  h1did  30782  rspsnid  32454  qsdrngilem  32561  erdszelem8  34127  neibastop2  35184  prnc  36873  proot1mul  41874  uneqsn  42709  mnuprdlem1  42964  islptre  44270  rrxsnicc  44951