MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snssg Structured version   Visualization version   GIF version

Theorem snssg 4296
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.
StepHypRef Expression
1 eleq1 2686 . 2 (𝑥 = 𝐴 → (𝑥𝐵𝐴𝐵))
2 sneq 4158 . . 3 (𝑥 = 𝐴 → {𝑥} = {𝐴})
32sseq1d 3611 . 2 (𝑥 = 𝐴 → ({𝑥} ⊆ 𝐵 ↔ {𝐴} ⊆ 𝐵))
4 vex 3189 . . 3 𝑥 ∈ V
54snss 4286 . 2 (𝑥𝐵 ↔ {𝑥} ⊆ 𝐵)
61, 3, 5vtoclbg 3253 1 (𝐴𝑉 → (𝐴𝐵 ↔ {𝐴} ⊆ 𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1480  wcel 1987  wss 3555  {csn 4148
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3188  df-in 3562  df-ss 3569  df-sn 4149
This theorem is referenced by:  tppreqb  4305  snssi  4308  prssg  4318  fvimacnvALT  6292  fr3nr  6926  vdwapid1  15603  acsfn  16241  cycsubg2  17552  cycsubg2cl  17553  pgpfac1lem1  18394  pgpfac1lem3a  18396  pgpfac1lem3  18397  pgpfac1lem5  18399  pgpfaclem2  18402  lspsnid  18912  lidldvgen  19174  isneip  20819  elnei  20825  iscnp4  20977  cnpnei  20978  nlly2i  21189  1stckgenlem  21266  flimopn  21689  flimclslem  21698  fclsneii  21731  fcfnei  21749  limcvallem  23541  ellimc2  23547  limcflf  23551  limccnp  23561  limccnp2  23562  limcco  23563  lhop2  23682  plyrem  23964  isppw  24740  lpvtx  25859  h1did  28256  erdszelem8  30885  neibastop2  31995  prnc  33495  proot1mul  37255  uneqsn  37800  islptre  39252  rrxsnicc  39824
  Copyright terms: Public domain W3C validator