Theorem snssg 4789

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2098  Vcvv 3461   ⊆ wss 3944  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-ss 3961  df-sn 4631

This theorem is referenced by:  snss  4791  tppreqb  4810  snssi  4813  prssg  4824  snelpwg  5444  relsng  5803  fvimacnvALT  7065  fr3nr  7775  vdwapid1  16947  acsfn  17642  cycsubg2  19173  cycsubg2cl  19174  pgpfac1lem1  20043  pgpfac1lem3a  20045  pgpfac1lem3  20046  pgpfac1lem5  20048  pgpfaclem2  20051  lspsnid  20889  lidldvgen  21241  isneip  23053  elnei  23059  iscnp4  23211  cnpnei  23212  nlly2i  23424  1stckgenlem  23501  flimopn  23923  flimclslem  23932  fclsneii  23965  fcfnei  23983  rrx0el  25370  limcvallem  25844  ellimc2  25850  limcflf  25854  limccnp  25864  limccnp2  25865  limcco  25866  lhop2  25992  plyrem  26285  isppw  27091  lpvtx  28953  h1did  31433  rspsnid  33183  dvdsrspss  33199  unitpidl1  33236  mxidlirred  33284  qsdrngilem  33306  evls1fldgencl  33489  erdszelem8  34939  neibastop2  35976  prnc  37671  proot1mul  42764  uneqsn  43597  mnuprdlem1  43851  islptre  45145  rrxsnicc  45826  sclnbgrelself  47320