Theorem snssg 4750

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2143  Vcvv 3455   ⊆ wss 3906  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3923  df-sn 4591

This theorem is referenced by:  snss  4751  snssi  4752  tppreqb  4774  prssg  4786  snelpwg  5426  relsng  5790  fvimacnvALT  7054  fr3nr  7772  sucprcreg  9569  vdwapid1  17036  acsfn  17716  cycsubg2  19282  cycsubg2cl  19283  pgpfac1lem1  20147  pgpfac1lem3a  20149  pgpfac1lem3  20150  pgpfac1lem5  20152  pgpfaclem2  20155  lspsnid  21095  rspsnid  21354  lidldvgen  21483  isneip  23243  elnei  23249  iscnp4  23401  cnpnei  23402  nlly2i  23614  1stckgenlem  23691  flimopn  24113  flimclslem  24122  fclsneii  24155  fcfnei  24173  rrx0el  25538  limcvallem  26011  ellimc2  26017  limcflf  26021  limccnp  26031  limccnp2  26032  limcco  26033  lhop2  26155  plyrem  26447  isppw  27259  lpvtx  29399  h1did  31884  prssad  32856  prssbd  32857  tpssg  32864  dvdsrspss  33681  unitpidl1  33713  mxidlirred  33736  qsdrngilem  33757  evls1fldgencl  34041  erdszelem8  35671  neibastop2  36853  prnc  38699  proot1mul  43904  uneqsn  44734  mnuprdlem1  44965  islptre  46318  rrxsnicc  46997  sclnbgrelself  48596