Theorem snssg 4747

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 4746	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
2	1	bicomi 227	. 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵)
3		elex 3474	. 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 2145  Vcvv 3453   ⊆ wss 3902  {csn 4587

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-ss 3919  df-sn 4588

This theorem is used by:  snss  4748  snssi  4749  tppreqb  4771  prssg  4783  snelpwg  5422  relsng  5786  fvimacnvALT  7053  fr3nr  7775  sucprcreg  9582  vdwapid1  17073  acsfn  17753  cycsubg2  19344  cycsubg2cl  19345  pgpfac1lem1  20209  pgpfac1lem3a  20211  pgpfac1lem3  20212  pgpfac1lem5  20214  pgpfaclem2  20217  lspsnid  21183  rspsnid  21442  lidldvgen  21571  isneip  23336  elnei  23342  iscnp4  23494  cnpnei  23495  nlly2i  23708  1stckgenlem  23785  flimopn  24207  flimclslem  24216  fclsneii  24249  fcfnei  24267  rrx0el  25632  limcvallem  26105  ellimc2  26111  limcflf  26115  limccnp  26125  limccnp2  26126  limcco  26127  lhop2  26249  plyrem  26542  isppw  27358  lpvtx  29533  h1did  32040  prssad  33012  prssbd  33013  tpssg  33020  dvdsrspss  33828  unitpidl1  33860  mxidlirred  33883  qsdrngilem  33904  evls1fldgencl  34188  erdszelem8  35785  neibastop2  36988  prnc  38825  proot1mul  44043  uneqsn  44873  mnuprdlem1  45104  islptre  46457  rrxsnicc  47136  sclnbgrelself  48772