Theorem snssg 4744

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 4743	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
2	1	bicomi 227	. 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵)
3		elex 3475	. 2 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ V)
4		imbibi 396	. 2 ⊢ (((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵) → (𝐴 ∈ V → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵)))
5	2, 3, 4	mpsyl 69	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2147  Vcvv 3454   ⊆ wss 3900  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-sn 4589

This theorem is used by:  snss  4745  snssi  4746  tppreqb  4768  prssg  4778  snelpwg  5416  relsng  5785  fvimacnvALT  7082  fr3nr  7813  sucprcreg  9630  vdwapid1  17185  acsfn  17865  cycsubg2  19457  cycsubg2cl  19458  pgpfac1lem1  20323  pgpfac1lem3a  20325  pgpfac1lem3  20326  pgpfac1lem5  20328  pgpfaclem2  20331  lspsnid  21301  rspsnid  21560  lidldvgen  21691  isneip  23456  elnei  23462  iscnp4  23614  cnpnei  23615  nlly2i  23828  1stckgenlem  23905  flimopn  24327  flimclslem  24336  fclsneii  24369  fcfnei  24387  rrx0el  25752  limcvallem  26224  ellimc2  26230  limcflf  26234  limccnp  26244  limccnp2  26245  limcco  26246  lhop2  26368  plyrem  26659  isppw  27474  lpvtx  29679  h1did  32186  prssad  33200  prssbd  33201  tpssg  33208  dvdsrspss  34026  unitpidl1  34058  mxidlirred  34081  qsdrngilem  34102  evls1fldgencl  34385  erdszelem8  36143  neibastop2  37340  prnc  39204  proot1mul  44399  uneqsn  45228  mnuprdlem1  45459  islptre  46846  rrxsnicc  47525  sclnbgrelself  49161