Theorem snssg 4808

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  Vcvv 3488   ⊆ wss 3976  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-sn 4649

This theorem is referenced by:  snss  4810  tppreqb  4830  snssi  4833  prssg  4844  snelpwg  5462  relsng  5825  fvimacnvALT  7090  fr3nr  7807  vdwapid1  17022  acsfn  17717  cycsubg2  19250  cycsubg2cl  19251  pgpfac1lem1  20118  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfac1lem5  20123  pgpfaclem2  20126  lspsnid  21014  lidldvgen  21367  isneip  23134  elnei  23140  iscnp4  23292  cnpnei  23293  nlly2i  23505  1stckgenlem  23582  flimopn  24004  flimclslem  24013  fclsneii  24046  fcfnei  24064  rrx0el  25451  limcvallem  25926  ellimc2  25932  limcflf  25936  limccnp  25946  limccnp2  25947  limcco  25948  lhop2  26074  plyrem  26365  isppw  27175  lpvtx  29103  h1did  31583  rspsnid  33364  dvdsrspss  33380  unitpidl1  33417  mxidlirred  33465  qsdrngilem  33487  evls1fldgencl  33680  erdszelem8  35166  neibastop2  36327  prnc  38027  proot1mul  43155  uneqsn  43987  mnuprdlem1  44241  islptre  45540  rrxsnicc  46221  sclnbgrelself  47720