Theorem snssg 4749

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 4748	. . 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 3916  {csn 4591

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 3933  df-sn 4592

This theorem is referenced by:  snss  4751  tppreqb  4771  snssi  4774  prssg  4785  snelpwg  5404  relsng  5766  fvimacnvALT  7031  fr3nr  7750  vdwapid1  16952  acsfn  17626  cycsubg2  19148  cycsubg2cl  19149  pgpfac1lem1  20012  pgpfac1lem3a  20014  pgpfac1lem3  20015  pgpfac1lem5  20017  pgpfaclem2  20020  lspsnid  20905  lidldvgen  21250  isneip  22998  elnei  23004  iscnp4  23156  cnpnei  23157  nlly2i  23369  1stckgenlem  23446  flimopn  23868  flimclslem  23877  fclsneii  23910  fcfnei  23928  rrx0el  25304  limcvallem  25778  ellimc2  25784  limcflf  25788  limccnp  25798  limccnp2  25799  limcco  25800  lhop2  25926  plyrem  26219  isppw  27030  lpvtx  29001  h1did  31486  prssad  32464  prssbd  32465  tpssg  32472  rspsnid  33348  dvdsrspss  33364  unitpidl1  33401  mxidlirred  33449  qsdrngilem  33471  evls1fldgencl  33671  erdszelem8  35185  neibastop2  36344  prnc  38056  proot1mul  43176  uneqsn  44007  mnuprdlem1  44254  islptre  45610  rrxsnicc  46291  sclnbgrelself  47838