Theorem snssg 4750

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  Vcvv 3450   ⊆ wss 3917  {csn 4592

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-ss 3934  df-sn 4593

This theorem is referenced by:  snss  4752  tppreqb  4772  snssi  4775  prssg  4786  snelpwg  5405  relsng  5767  fvimacnvALT  7032  fr3nr  7751  vdwapid1  16953  acsfn  17627  cycsubg2  19149  cycsubg2cl  19150  pgpfac1lem1  20013  pgpfac1lem3a  20015  pgpfac1lem3  20016  pgpfac1lem5  20018  pgpfaclem2  20021  lspsnid  20906  lidldvgen  21251  isneip  22999  elnei  23005  iscnp4  23157  cnpnei  23158  nlly2i  23370  1stckgenlem  23447  flimopn  23869  flimclslem  23878  fclsneii  23911  fcfnei  23929  rrx0el  25305  limcvallem  25779  ellimc2  25785  limcflf  25789  limccnp  25799  limccnp2  25800  limcco  25801  lhop2  25927  plyrem  26220  isppw  27031  lpvtx  29002  h1did  31487  prssad  32465  prssbd  32466  tpssg  32473  rspsnid  33349  dvdsrspss  33365  unitpidl1  33402  mxidlirred  33450  qsdrngilem  33472  evls1fldgencl  33672  erdszelem8  35192  neibastop2  36356  prnc  38068  proot1mul  43190  uneqsn  44021  mnuprdlem1  44268  islptre  45624  rrxsnicc  46305  sclnbgrelself  47852