Theorem snssg 4783

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  Vcvv 3480   ⊆ wss 3951  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-sn 4627

This theorem is referenced by:  snss  4785  tppreqb  4805  snssi  4808  prssg  4819  snelpwg  5447  relsng  5811  fvimacnvALT  7077  fr3nr  7792  vdwapid1  17013  acsfn  17702  cycsubg2  19228  cycsubg2cl  19229  pgpfac1lem1  20094  pgpfac1lem3a  20096  pgpfac1lem3  20097  pgpfac1lem5  20099  pgpfaclem2  20102  lspsnid  20991  lidldvgen  21344  isneip  23113  elnei  23119  iscnp4  23271  cnpnei  23272  nlly2i  23484  1stckgenlem  23561  flimopn  23983  flimclslem  23992  fclsneii  24025  fcfnei  24043  rrx0el  25432  limcvallem  25906  ellimc2  25912  limcflf  25916  limccnp  25926  limccnp2  25927  limcco  25928  lhop2  26054  plyrem  26347  isppw  27157  lpvtx  29085  h1did  31570  rspsnid  33399  dvdsrspss  33415  unitpidl1  33452  mxidlirred  33500  qsdrngilem  33522  evls1fldgencl  33720  erdszelem8  35203  neibastop2  36362  prnc  38074  proot1mul  43206  uneqsn  44038  mnuprdlem1  44291  islptre  45634  rrxsnicc  46315  sclnbgrelself  47834