Theorem snssg 4469

Description: The singleton of an element of a class is a subset of the class (general form of snss 4470). 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 4350	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	imbi1i 340	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3	2	albii 1914	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
4	3	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
5		dfss2 3749	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)))
7		clel2g 3492	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
8	4, 6, 7	3bitr4rd 303	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 197  ∀wal 1650   = wceq 1652   ∈ wcel 2155   ⊆ wss 3732  {csn 4334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-in 3739  df-ss 3746  df-sn 4335

This theorem is referenced by:  snss  4470  tppreqb  4490  snssi  4493  prssg  4504  relsng  5392  fvimacnvALT  6526  fr3nr  7177  vdwapid1  15958  acsfn  16585  cycsubg2  17895  cycsubg2cl  17896  pgpfac1lem1  18740  pgpfac1lem3a  18742  pgpfac1lem3  18743  pgpfac1lem5  18745  pgpfaclem2  18748  lspsnid  19265  lidldvgen  19529  isneip  21189  elnei  21195  iscnp4  21347  cnpnei  21348  nlly2i  21559  1stckgenlem  21636  flimopn  22058  flimclslem  22067  fclsneii  22100  fcfnei  22118  limcvallem  23926  ellimc2  23932  limcflf  23936  limccnp  23946  limccnp2  23947  limcco  23948  lhop2  24069  plyrem  24351  isppw  25131  lpvtx  26240  h1did  28866  erdszelem8  31628  neibastop2  32799  prnc  34288  proot1mul  38454  uneqsn  38995  islptre  40489  rrxsnicc  41157