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 3472	. 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 3451   ⊆ wss 3899  {csn 4584

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-ss 3916  df-sn 4585

This theorem is used by:  snss  4745  snssi  4746  tppreqb  4768  prssg  4780  snelpwg  5411  relsng  5779  fvimacnvALT  7048  fr3nr  7775  sucprcreg  9584  vdwapid1  17133  acsfn  17813  cycsubg2  19405  cycsubg2cl  19406  pgpfac1lem1  20270  pgpfac1lem3a  20272  pgpfac1lem3  20273  pgpfac1lem5  20275  pgpfaclem2  20278  lspsnid  21248  rspsnid  21507  lidldvgen  21638  isneip  23403  elnei  23409  iscnp4  23561  cnpnei  23562  nlly2i  23775  1stckgenlem  23852  flimopn  24274  flimclslem  24283  fclsneii  24316  fcfnei  24334  rrx0el  25699  limcvallem  26171  ellimc2  26177  limcflf  26181  limccnp  26191  limccnp2  26192  limcco  26193  lhop2  26315  plyrem  26608  isppw  27423  lpvtx  29628  h1did  32135  prssad  33107  prssbd  33108  tpssg  33115  dvdsrspss  33924  unitpidl1  33956  mxidlirred  33979  qsdrngilem  34000  evls1fldgencl  34284  erdszelem8  35932  neibastop2  37119  prnc  38969  proot1mul  44154  uneqsn  44984  mnuprdlem1  45215  islptre  46575  rrxsnicc  47254  sclnbgrelself  48890