Theorem snssg 4737

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  Vcvv 3438   ⊆ wss 3905  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-ss 3922  df-sn 4580

This theorem is referenced by:  snss  4739  tppreqb  4759  snssi  4762  prssg  4773  snelpwg  5389  relsng  5748  fvimacnvALT  6995  fr3nr  7712  vdwapid1  16905  acsfn  17583  cycsubg2  19107  cycsubg2cl  19108  pgpfac1lem1  19973  pgpfac1lem3a  19975  pgpfac1lem3  19976  pgpfac1lem5  19978  pgpfaclem2  19981  lspsnid  20914  lidldvgen  21259  isneip  23008  elnei  23014  iscnp4  23166  cnpnei  23167  nlly2i  23379  1stckgenlem  23456  flimopn  23878  flimclslem  23887  fclsneii  23920  fcfnei  23938  rrx0el  25314  limcvallem  25788  ellimc2  25794  limcflf  25798  limccnp  25808  limccnp2  25809  limcco  25810  lhop2  25936  plyrem  26229  isppw  27040  lpvtx  29031  h1did  31513  prssad  32491  prssbd  32492  tpssg  32499  rspsnid  33318  dvdsrspss  33334  unitpidl1  33371  mxidlirred  33419  qsdrngilem  33441  evls1fldgencl  33641  erdszelem8  35170  neibastop2  36334  prnc  38046  proot1mul  43167  uneqsn  43998  mnuprdlem1  44245  islptre  45601  rrxsnicc  46282  sclnbgrelself  47833