Theorem snssg 4740

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 4739	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ (𝐴 ∈ V → 𝐴 ∈ 𝐵))
2	1	bicomi 227	. 2 ⊢ ((𝐴 ∈ V → 𝐴 ∈ 𝐵) ↔ {𝐴} ⊆ 𝐵)
3		elex 3471	. 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 2144  Vcvv 3450   ⊆ wss 3895  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-sn 4585

This theorem is used by:  snss  4741  snssi  4742  tppreqb  4764  prssg  4774  snelpwg  5410  relsng  5778  fvimacnvALT  7057  fr3nr  7787  sucprcreg  9604  vdwapid1  17159  acsfn  17839  cycsubg2  19431  cycsubg2cl  19432  pgpfac1lem1  20296  pgpfac1lem3a  20298  pgpfac1lem3  20299  pgpfac1lem5  20301  pgpfaclem2  20304  lspsnid  21274  rspsnid  21533  lidldvgen  21664  isneip  23429  elnei  23435  iscnp4  23587  cnpnei  23588  nlly2i  23801  1stckgenlem  23878  flimopn  24300  flimclslem  24309  fclsneii  24342  fcfnei  24360  rrx0el  25725  limcvallem  26197  ellimc2  26203  limcflf  26207  limccnp  26217  limccnp2  26218  limcco  26219  lhop2  26341  plyrem  26632  isppw  27447  lpvtx  29652  h1did  32159  prssad  33173  prssbd  33174  tpssg  33181  dvdsrspss  33989  unitpidl1  34021  mxidlirred  34044  qsdrngilem  34065  evls1fldgencl  34349  erdszelem8  36050  neibastop2  37242  prnc  39095  proot1mul  44290  uneqsn  45119  mnuprdlem1  45350  islptre  46725  rrxsnicc  47404  sclnbgrelself  49040