Theorem snssg 4698

Description: The singleton of an element of a class is a subset of the class (general form of snss 4699). 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 4557	. . . . 5 ⊢ (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
2	1	imbi1i 353	. . . 4 ⊢ ((𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ (𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
3	2	albii 1827	. . 3 ⊢ (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵))
4	3	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵) ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
5		dfss2 3886	. . 3 ⊢ ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵))
6	5	a1i 11	. 2 ⊢ (𝐴 ∈ 𝑉 → ({𝐴} ⊆ 𝐵 ↔ ∀𝑥(𝑥 ∈ {𝐴} → 𝑥 ∈ 𝐵)))
7		clel2g 3566	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ ∀𝑥(𝑥 = 𝐴 → 𝑥 ∈ 𝐵)))
8	4, 6, 7	3bitr4rd 315	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1541   = wceq 1543   ∈ wcel 2110   ⊆ wss 3866  {csn 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883  df-sn 4542

This theorem is referenced by:  snss  4699  tppreqb  4718  snssi  4721  prssg  4732  relsng  5671  fvimacnvALT  6877  fr3nr  7557  vdwapid1  16528  acsfn  17162  cycsubg2  18617  cycsubg2cl  18618  pgpfac1lem1  19461  pgpfac1lem3a  19463  pgpfac1lem3  19464  pgpfac1lem5  19466  pgpfaclem2  19469  lspsnid  20030  lidldvgen  20293  isneip  22002  elnei  22008  iscnp4  22160  cnpnei  22161  nlly2i  22373  1stckgenlem  22450  flimopn  22872  flimclslem  22881  fclsneii  22914  fcfnei  22932  rrx0el  24295  limcvallem  24768  ellimc2  24774  limcflf  24778  limccnp  24788  limccnp2  24789  limcco  24790  lhop2  24912  plyrem  25198  isppw  25996  lpvtx  27159  h1did  29632  rspsnid  31282  erdszelem8  32873  neibastop2  34287  prnc  35962  proot1mul  40727  uneqsn  41310  mnuprdlem1  41563  islptre  42835  rrxsnicc  43516