Theorem snssg 4747

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  Vcvv 3447   ⊆ wss 3914  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-ss 3931  df-sn 4590

This theorem is referenced by:  snss  4749  tppreqb  4769  snssi  4772  prssg  4783  snelpwg  5402  relsng  5764  fvimacnvALT  7029  fr3nr  7748  vdwapid1  16946  acsfn  17620  cycsubg2  19142  cycsubg2cl  19143  pgpfac1lem1  20006  pgpfac1lem3a  20008  pgpfac1lem3  20009  pgpfac1lem5  20011  pgpfaclem2  20014  lspsnid  20899  lidldvgen  21244  isneip  22992  elnei  22998  iscnp4  23150  cnpnei  23151  nlly2i  23363  1stckgenlem  23440  flimopn  23862  flimclslem  23871  fclsneii  23904  fcfnei  23922  rrx0el  25298  limcvallem  25772  ellimc2  25778  limcflf  25782  limccnp  25792  limccnp2  25793  limcco  25794  lhop2  25920  plyrem  26213  isppw  27024  lpvtx  28995  h1did  31480  prssad  32458  prssbd  32459  tpssg  32466  rspsnid  33342  dvdsrspss  33358  unitpidl1  33395  mxidlirred  33443  qsdrngilem  33465  evls1fldgencl  33665  erdszelem8  35185  neibastop2  36349  prnc  38061  proot1mul  43183  uneqsn  44014  mnuprdlem1  44261  islptre  45617  rrxsnicc  46298  sclnbgrelself  47848