MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snex Unicode version

Theorem snex 4693
Description: A singleton is a set. Theorem 7.12 of [Quine] p. 51, proved using Extensionality, Separation, Null Set, and Pairing. See also snexALT 4638. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.)
Assertion
Ref Expression
snex

Proof of Theorem snex
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfsn2 4042 . . 3
2 preq12 4111 . . . . . 6
32anidms 645 . . . . 5
43eleq1d 2526 . . . 4
5 zfpair2 4692 . . . 4
64, 5vtoclg 3167 . . 3
71, 6syl5eqel 2549 . 2
8 snprc 4093 . . . 4
98biimpi 194 . . 3
10 0ex 4582 . . 3
119, 10syl6eqel 2553 . 2
127, 11pm2.61i 164 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  =wceq 1395  e.wcel 1818   cvv 3109   c0 3784  {csn 4029  {cpr 4031
This theorem is referenced by:  prex  4694  elALT  4695  dtruALT2  4696  snelpwi  4697  snelpw  4698  rext  4700  sspwb  4701  intid  4710  moabex  4711  nnullss  4714  exss  4715  opi1  4719  op1stb  4722  opnz  4723  opeqsn  4748  opeqpr  4749  opthwiener  4754  uniop  4755  frirr  4861  frsn  5075  onnev  5089  xpsspwOLD  5122  relop  5158  funopg  5625  tpex  6599  snnex  6606  difsnexi  6608  sucexb  6644  soex  6743  elxp4  6744  elxp5  6745  opabex3d  6778  opabex3  6779  1stval  6802  2ndval  6803  fo1st  6820  fo2nd  6821  mpt2exxg  6874  cnvf1o  6899  fnse  6917  suppsnop  6932  brtpos2  6980  tfrlem12  7077  tfrlem16  7081  mapsn  7480  fvdiagfn  7483  mapsnconst  7484  mapsncnv  7485  mapsnf1o2  7486  ralxpmap  7488  elixpsn  7528  ixpsnf1o  7529  mapsnf1o  7530  ensn1  7599  en1b  7603  mapsnen  7613  xpsnen  7621  endisj  7624  xpsnen2g  7630  domunsncan  7637  enfixsn  7646  domunsn  7687  fodomr  7688  disjenex  7695  domssex2  7697  domssex  7698  map2xp  7707  phplem2  7717  isinf  7753  pssnn  7758  findcard2  7780  ac6sfi  7784  xpfi  7811  fodomfi  7819  pwfilem  7834  fczfsuppd  7867  snopfsupp  7872  fisn  7907  marypha1lem  7913  brwdom2  8020  unxpwdom2  8035  elirrv  8044  epfrs  8183  tc2  8194  tcsni  8195  ranksuc  8304  fseqenlem1  8426  dfac5lem2  8526  dfac5lem3  8527  dfac5lem4  8528  kmlem2  8552  cdafn  8570  cdaval  8571  cdaassen  8583  mapcdaen  8585  cdadom1  8587  cdainf  8593  ackbij1lem5  8625  cfsuc  8658  isfin1-3  8787  hsmexlem4  8830  axcc2lem  8837  dcomex  8848  axdc3lem4  8854  axdc4lem  8856  ttukeylem3  8912  brdom7disj  8930  brdom6disj  8931  fpwwe2lem13  9041  canthwe  9050  canthp1lem1  9051  uniwun  9139  rankcf  9176  nn0ex  10826  hashxplem  12491  hashmap  12493  hashbclem  12501  hashf1lem1  12504  hashge3el3dif  12524  climconst2  13371  incexclem  13648  ramub1lem2  14545  cshwsex  14585  setsvalg  14655  setsid  14673  pwsbas  14884  pwsle  14889  pwssca  14893  pwssnf1o  14895  imasplusg  14914  imasmulr  14915  imasvsca  14917  imasip  14918  xpsc  14954  acsfn  15056  isfunc  15233  homaf  15357  homaval  15358  mgm1  15884  sgrp1  15918  mnd1  15961  mnd1OLD  15962  mnd1id  15963  grp1  16142  symg2bas  16423  idrespermg  16436  pmtrsn  16544  psgnsn  16545  abl1  16872  gsum2d2  17002  gsumcom2  17003  dprdz  17077  dprdsn  17083  dprd2da  17091  ring1  17248  pwssplit3  17707  drngnidl  17877  drnglpir  17901  rng1nnzr  17922  evlssca  18191  mpfind  18205  evls1sca  18360  pf1ind  18391  frlmip  18809  islindf4  18873  mattposvs  18957  mat1dimelbas  18973  mat1dimscm  18977  mat1dimmul  18978  mat1rhmval  18981  m1detdiag  19099  mdetrlin  19104  mdetrsca2  19106  mdetrlin2  19109  mdetunilem5  19118  smadiadetglem2  19174  basdif0  19454  ordtbas  19693  leordtval2  19713  dishaus  19883  discmp  19898  concompid  19932  dis2ndc  19961  dislly  19998  dis1stc  20000  unisngl  20028  1stckgen  20055  ptbasfi  20082  dfac14lem  20118  dfac14  20119  ptrescn  20140  xkoptsub  20155  pt1hmeo  20307  xpstopnlem1  20310  ptcmpfi  20314  isufil2  20409  ufileu  20420  filufint  20421  uffix  20422  uffixsn  20426  flimclslem  20485  ptcmplem1  20552  cnextfval  20562  imasdsf1olem  20876  icccmplem1  21327  icccmplem2  21328  rrxip  21822  elply2  22593  plyss  22596  plyeq0lem  22607  taylfval  22754  axlowdimlem15  24259  axlowdim  24264  umgra1  24326  uslgra1  24372  usgra1  24373  usgra1v  24390  cusgra1v  24461  uvtx01vtx  24492  wlkntrl  24564  0pthonv  24583  constr1trl  24590  1pthon  24593  1pthon2v  24595  1conngra  24675  vdgr1d  24903  vdgr1b  24904  vdgr1a  24906  grposn  25217  zrdivrng  25434  0ofval  25702  resf1o  27553  ordtconlem1  27906  esumpr  28073  esumfzf  28075  prsiga  28131  cntnevol  28199  eulerpartlemgs2  28319  ccatmulgnn0dir  28496  ofs1  28499  ofcs1  28500  subfacp1lem5  28628  erdszelem5  28639  erdszelem8  28642  cvmliftlem4  28733  cvmliftlem5  28734  cvmlift2lem6  28753  cvmlift2lem9  28756  cvmlift2lem12  28759  wfrlem15  29357  fobigcup  29550  elsingles  29568  fnsingle  29569  fvsingle  29570  dfiota3  29573  brapply  29588  brsuccf  29591  funpartlem  29592  altopthsn  29611  altxpsspw  29627  hfsn  29836  onpsstopbas  29895  finixpnum  30038  ptrest  30048  neibastop2lem  30178  topjoin  30183  fdc  30238  heiborlem3  30309  heiborlem8  30314  ismrer1  30334  elrfi  30626  mzpincl  30666  mzpcompact2lem  30684  wopprc  30972  dfac11  31008  kelac2  31011  pwslnmlem1  31038  pwslnm  31040  fnchoice  31404  limcresiooub  31648  limcresioolb  31649  cnfdmsn  31684  dvsinax  31708  fourierdlem48  31937  fourierdlem49  31938  funcsetcestrclem1  32660  mpt2exxg2  32927  mapsnop  32934  lindsrng01  33069  snlindsntorlem  33071  snlindsntor  33072  lmod1lem1  33088  lmod1lem2  33089  lmod1lem3  33090  lmod1lem4  33091  lmod1lem5  33092  lmod1  33093  lmod1zr  33094  aacllem  33216  snelpwrVD  33631  bnj918  33824  bnj95  33922  bnj1452  34108  bnj1489  34112  bj-sels  34520  bj-snsetex  34521  bj-elsngl  34526  bj-2uplex  34580  bj-elopg  34602  ldualset  34850  lineset  35462  ispointN  35466  dvaset  36731  dvhset  36808  dibval  36869  dibfna  36881
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-un 3480  df-nul 3785  df-sn 4030  df-pr 4032
  Copyright terms: Public domain W3C validator