Theorem snssg 4759

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  Vcvv 3459   ⊆ wss 3926  {csn 4601

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-ss 3943  df-sn 4602

This theorem is referenced by:  snss  4761  tppreqb  4781  snssi  4784  prssg  4795  snelpwg  5417  relsng  5780  fvimacnvALT  7047  fr3nr  7766  vdwapid1  16995  acsfn  17671  cycsubg2  19193  cycsubg2cl  19194  pgpfac1lem1  20057  pgpfac1lem3a  20059  pgpfac1lem3  20060  pgpfac1lem5  20062  pgpfaclem2  20065  lspsnid  20950  lidldvgen  21295  isneip  23043  elnei  23049  iscnp4  23201  cnpnei  23202  nlly2i  23414  1stckgenlem  23491  flimopn  23913  flimclslem  23922  fclsneii  23955  fcfnei  23973  rrx0el  25350  limcvallem  25824  ellimc2  25830  limcflf  25834  limccnp  25844  limccnp2  25845  limcco  25846  lhop2  25972  plyrem  26265  isppw  27076  lpvtx  29047  h1did  31532  prssad  32510  prssbd  32511  tpssg  32518  rspsnid  33386  dvdsrspss  33402  unitpidl1  33439  mxidlirred  33487  qsdrngilem  33509  evls1fldgencl  33711  erdszelem8  35220  neibastop2  36379  prnc  38091  proot1mul  43218  uneqsn  44049  mnuprdlem1  44296  islptre  45648  rrxsnicc  46329  sclnbgrelself  47861