Theorem snssg 4735

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  Vcvv 3437   ⊆ wss 3898  {csn 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-ss 3915  df-sn 4576

This theorem is referenced by:  snss  4736  tppreqb  4756  snssi  4759  prssg  4770  snelpwg  5386  relsng  5745  fvimacnvALT  6996  fr3nr  7711  vdwapid1  16889  acsfn  17567  cycsubg2  19124  cycsubg2cl  19125  pgpfac1lem1  19990  pgpfac1lem3a  19992  pgpfac1lem3  19993  pgpfac1lem5  19995  pgpfaclem2  19998  lspsnid  20928  lidldvgen  21273  isneip  23021  elnei  23027  iscnp4  23179  cnpnei  23180  nlly2i  23392  1stckgenlem  23469  flimopn  23891  flimclslem  23900  fclsneii  23933  fcfnei  23951  rrx0el  25326  limcvallem  25800  ellimc2  25806  limcflf  25810  limccnp  25820  limccnp2  25821  limcco  25822  lhop2  25948  plyrem  26241  isppw  27052  lpvtx  29048  h1did  31533  prssad  32511  prssbd  32512  tpssg  32519  rspsnid  33343  dvdsrspss  33359  unitpidl1  33396  mxidlirred  33444  qsdrngilem  33466  evls1fldgencl  33704  erdszelem8  35263  neibastop2  36426  prnc  38127  proot1mul  43311  uneqsn  44142  mnuprdlem1  44389  islptre  45743  rrxsnicc  46422  sclnbgrelself  47972