Theorem snssg 4722

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

Syntax hints:   → wi 4   ↔ wb 207   ∈ wcel 2119  Vcvv 3432   ⊆ wss 3890  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-ss 3907  df-sn 4563

This theorem is referenced by:  snss  4723  snssi  4724  tppreqb  4745  prssg  4757  snelpwg  5389  relsng  5751  fvimacnvALT  7005  fr3nr  7722  sucprcreg  9518  vdwapid1  16944  acsfn  17623  cycsubg2  19183  cycsubg2cl  19184  pgpfac1lem1  20049  pgpfac1lem3a  20051  pgpfac1lem3  20052  pgpfac1lem5  20054  pgpfaclem2  20057  lspsnid  20990  lidldvgen  21334  isneip  23095  elnei  23101  iscnp4  23253  cnpnei  23254  nlly2i  23466  1stckgenlem  23543  flimopn  23965  flimclslem  23974  fclsneii  24007  fcfnei  24025  rrx0el  25390  limcvallem  25863  ellimc2  25869  limcflf  25873  limccnp  25883  limccnp2  25884  limcco  25885  lhop2  26007  plyrem  26296  isppw  27102  lpvtx  29162  h1did  31647  prssad  32624  prssbd  32625  tpssg  32632  rspsnid  33461  dvdsrspss  33477  unitpidl1  33514  mxidlirred  33562  qsdrngilem  33584  evls1fldgencl  33861  erdszelem8  35433  neibastop2  36596  prnc  38441  proot1mul  43646  uneqsn  44476  mnuprdlem1  44723  islptre  46071  rrxsnicc  46750  sclnbgrelself  48346