Theorem snssg 4727

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  Vcvv 3429   ⊆ wss 3889  {csn 4567

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-sn 4568

This theorem is referenced by:  snss  4728  snssi  4729  tppreqb  4750  prssg  4762  snelpwg  5395  relsng  5757  fvimacnvALT  7009  fr3nr  7726  sucprcreg  9520  vdwapid1  16946  acsfn  17625  cycsubg2  19185  cycsubg2cl  19186  pgpfac1lem1  20051  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem5  20056  pgpfaclem2  20059  lspsnid  20988  lidldvgen  21332  isneip  23070  elnei  23076  iscnp4  23228  cnpnei  23229  nlly2i  23441  1stckgenlem  23518  flimopn  23940  flimclslem  23949  fclsneii  23982  fcfnei  24000  rrx0el  25365  limcvallem  25838  ellimc2  25844  limcflf  25848  limccnp  25858  limccnp2  25859  limcco  25860  lhop2  25982  plyrem  26271  isppw  27077  lpvtx  29137  h1did  31622  prssad  32599  prssbd  32600  tpssg  32607  rspsnid  33431  dvdsrspss  33447  unitpidl1  33484  mxidlirred  33532  qsdrngilem  33554  evls1fldgencl  33814  erdszelem8  35380  neibastop2  36543  prnc  38388  proot1mul  43622  uneqsn  44452  mnuprdlem1  44699  islptre  46049  rrxsnicc  46728  sclnbgrelself  48324