Theorem snssg 4788

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2106  Vcvv 3478   ⊆ wss 3963  {csn 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-ss 3980  df-sn 4632

This theorem is referenced by:  snss  4790  tppreqb  4810  snssi  4813  prssg  4824  snelpwg  5453  relsng  5814  fvimacnvALT  7077  fr3nr  7791  vdwapid1  17009  acsfn  17704  cycsubg2  19241  cycsubg2cl  19242  pgpfac1lem1  20109  pgpfac1lem3a  20111  pgpfac1lem3  20112  pgpfac1lem5  20114  pgpfaclem2  20117  lspsnid  21009  lidldvgen  21362  isneip  23129  elnei  23135  iscnp4  23287  cnpnei  23288  nlly2i  23500  1stckgenlem  23577  flimopn  23999  flimclslem  24008  fclsneii  24041  fcfnei  24059  rrx0el  25446  limcvallem  25921  ellimc2  25927  limcflf  25931  limccnp  25941  limccnp2  25942  limcco  25943  lhop2  26069  plyrem  26362  isppw  27172  lpvtx  29100  h1did  31580  rspsnid  33379  dvdsrspss  33395  unitpidl1  33432  mxidlirred  33480  qsdrngilem  33502  evls1fldgencl  33695  erdszelem8  35183  neibastop2  36344  prnc  38054  proot1mul  43183  uneqsn  44015  mnuprdlem1  44268  islptre  45575  rrxsnicc  46256  sclnbgrelself  47772