Theorem snssg 4709

Description: The singleton of an element of a class is a subset of the class (general form of snss 4710). Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.)

Assertion

Ref	Expression
snssg	⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Proof of Theorem snssg

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		velsn 4575	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	imbi1i 352	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3	2	albii 1814	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
4	3	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
5		dfss2 3953	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)))
7		clel2g 3650	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
8	4, 6, 7	3bitr4rd 314	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 208  ∀wal 1529   = wceq 1531   ∈ wcel 2108   ⊆ wss 3934  {csn 4559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-v 3495  df-in 3941  df-ss 3950  df-sn 4560

This theorem is referenced by:  snss  4710  tppreqb  4730  snssi  4733  prssg  4744  relsng  5667  fvimacnvALT  6820  fr3nr  7486  vdwapid1  16303  acsfn  16922  cycsubg2  18345  cycsubg2cl  18346  pgpfac1lem1  19188  pgpfac1lem3a  19190  pgpfac1lem3  19191  pgpfac1lem5  19193  pgpfaclem2  19196  lspsnid  19757  lidldvgen  20020  isneip  21705  elnei  21711  iscnp4  21863  cnpnei  21864  nlly2i  22076  1stckgenlem  22153  flimopn  22575  flimclslem  22584  fclsneii  22617  fcfnei  22635  rrx0el  23993  limcvallem  24461  ellimc2  24467  limcflf  24471  limccnp  24481  limccnp2  24482  limcco  24483  lhop2  24604  plyrem  24886  isppw  25683  lpvtx  26845  h1did  29320  rspsnid  30930  erdszelem8  32438  neibastop2  33702  prnc  35337  proot1mul  39789  uneqsn  40363  mnuprdlem1  40598  islptre  41889  rrxsnicc  42575