Theorem snssg 4736

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2111  Vcvv 3436   ⊆ wss 3902  {csn 4576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-ss 3919  df-sn 4577

This theorem is referenced by:  snss  4737  tppreqb  4757  snssi  4760  prssg  4771  snelpwg  5384  relsng  5741  fvimacnvALT  6990  fr3nr  7705  vdwapid1  16884  acsfn  17562  cycsubg2  19120  cycsubg2cl  19121  pgpfac1lem1  19986  pgpfac1lem3a  19988  pgpfac1lem3  19989  pgpfac1lem5  19991  pgpfaclem2  19994  lspsnid  20924  lidldvgen  21269  isneip  23018  elnei  23024  iscnp4  23176  cnpnei  23177  nlly2i  23389  1stckgenlem  23466  flimopn  23888  flimclslem  23897  fclsneii  23930  fcfnei  23948  rrx0el  25323  limcvallem  25797  ellimc2  25803  limcflf  25807  limccnp  25817  limccnp2  25818  limcco  25819  lhop2  25945  plyrem  26238  isppw  27049  lpvtx  29044  h1did  31526  prssad  32504  prssbd  32505  tpssg  32512  rspsnid  33331  dvdsrspss  33347  unitpidl1  33384  mxidlirred  33432  qsdrngilem  33454  evls1fldgencl  33678  erdszelem8  35230  neibastop2  36394  prnc  38106  proot1mul  43226  uneqsn  44057  mnuprdlem1  44304  islptre  45658  rrxsnicc  46337  sclnbgrelself  47878