Theorem snssg 4327

Description: The singleton of an element of a class is a subset of the class. 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		eleq1 2689	. 2 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ 𝐵 ↔ 𝐴 ∈ 𝐵))
2		sneq 4187	. . 3 ⊢ (𝑥 = 𝐴 → {𝑥} = {𝐴})
3	2	sseq1d 3632	. 2 ⊢ (𝑥 = 𝐴 → ({𝑥} ⊆ 𝐵 ↔ {𝐴} ⊆ 𝐵))
4		vex 3203	. . 3 ⊢ 𝑥 ∈ V
5	4	snss 4316	. 2 ⊢ (𝑥 ∈ 𝐵 ↔ {𝑥} ⊆ 𝐵)
6	1, 3, 5	vtoclbg 3267	1 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))

Syntax hints:   → wi 4   ↔ wb 196   = wceq 1483   ∈ wcel 1990   ⊆ wss 3574  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-sn 4178

This theorem is referenced by:  tppreqb  4336  snssi  4339  prssg  4350  fvimacnvALT  6336  fr3nr  6979  vdwapid1  15679  acsfn  16320  cycsubg2  17631  cycsubg2cl  17632  pgpfac1lem1  18473  pgpfac1lem3a  18475  pgpfac1lem3  18476  pgpfac1lem5  18478  pgpfaclem2  18481  lspsnid  18993  lidldvgen  19255  isneip  20909  elnei  20915  iscnp4  21067  cnpnei  21068  nlly2i  21279  1stckgenlem  21356  flimopn  21779  flimclslem  21788  fclsneii  21821  fcfnei  21839  limcvallem  23635  ellimc2  23641  limcflf  23645  limccnp  23655  limccnp2  23656  limcco  23657  lhop2  23778  plyrem  24060  isppw  24840  lpvtx  25963  h1did  28410  erdszelem8  31180  neibastop2  32356  prnc  33866  proot1mul  37777  uneqsn  38321  islptre  39851  rrxsnicc  40520