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

Theorem snex 4373
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4353. (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 19-May-2013.) (Proof modification is discouraged.)
Assertion
Ref Expression
snex  |-  { A }  e.  _V

Proof of Theorem snex
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 dfsn2 3796 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3853 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 627 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2478 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4372 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 2979 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2496 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3839 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 187 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4307 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2500 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 158 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1649    e. wcel 1721   _Vcvv 2924   (/)c0 3596   {csn 3782   {cpr 3783
This theorem is referenced by:  prex  4374  elALT  4375  dtruALT2  4376  snelpwi  4377  snelpw  4378  rext  4380  sspwb  4381  intid  4389  moabex  4390  nnullss  4393  exss  4394  opi1  4398  opnz  4400  opeqsn  4420  opeqpr  4421  opthwiener  4426  uniop  4427  frirr  4527  tpex  4675  snnex  4680  op1stb  4725  sucexb  4756  frsn  4915  onnev  4925  xpsspwOLD  4954  relop  4990  soex  5286  elxp4  5324  elxp5  5325  funopg  5452  opabex3d  5956  opabex3  5957  1stval  6318  2ndval  6319  fo1st  6333  fo2nd  6334  mpt2exxg  6389  cnvf1o  6412  fnse  6430  brtpos2  6452  tfrlem12  6617  tfrlem16  6621  mapsn  7022  fvdiagfn  7025  mapsnconst  7026  mapsncnv  7027  mapsnf1o2  7028  elixpsn  7068  ixpsnf1o  7069  mapsnf1o  7070  ensn1  7138  en1b  7142  mapsnen  7151  xpsnen  7159  endisj  7162  xpsnen2g  7168  domunsncan  7175  domunsn  7224  fodomr  7225  disjenex  7232  domssex2  7234  domssex  7235  map2xp  7244  phplem2  7254  isinf  7289  pssnn  7294  findcard2  7315  ac6sfi  7318  xpfi  7345  fodomfi  7352  pwfilem  7367  fisn  7398  marypha1lem  7404  brwdom2  7505  unxpwdom2  7520  elirrv  7529  epfrs  7631  tc2  7645  tcsni  7646  ranksuc  7755  fseqenlem1  7869  dfac5lem2  7969  dfac5lem3  7970  dfac5lem4  7971  kmlem2  7995  cdafn  8013  cdaval  8014  cdaassen  8026  mapcdaen  8028  cdadom1  8030  cdainf  8036  ackbij1lem5  8068  cfsuc  8101  isfin1-3  8230  hsmexlem4  8273  axcc2lem  8280  dcomex  8291  axdc3lem4  8297  axdc4lem  8299  ttukeylem3  8355  brdom7disj  8373  brdom6disj  8374  fpwwe2lem13  8481  canthwe  8490  canthp1lem1  8491  uniwun  8579  rankcf  8616  nn0ex  10191  hashxplem  11659  hashmap  11661  hashbclem  11664  hashf1lem1  11667  climconst2  12305  incexclem  12579  ramub1lem2  13358  setsvalg  13455  setsid  13471  pwsbas  13672  pwsle  13677  pwssca  13681  pwssnf1o  13683  imasplusg  13706  imasmulr  13707  imasvsca  13709  xpsc  13745  acsfn  13847  isfunc  14024  homaf  14148  homaval  14149  gsum2d2  15511  gsumcom2  15512  dprdz  15551  dprdsn  15557  dprd2da  15563  drngnidl  16263  drnglpir  16287  basdif0  16981  ordtbas  17218  leordtval2  17238  dishaus  17408  discmp  17423  concompid  17455  dis2ndc  17484  dislly  17521  dis1stc  17523  1stckgen  17547  ptbasfi  17574  dfac14lem  17610  dfac14  17611  ptrescn  17632  xkoptsub  17647  pt1hmeo  17799  xpstopnlem1  17802  ptcmpfi  17806  isufil2  17901  ufileu  17912  filufint  17913  uffix  17914  uffixsn  17918  flimclslem  17977  ptcmplem1  18044  cnextfval  18054  imasdsf1olem  18364  icccmplem1  18814  icccmplem2  18815  evlssca  19904  mpfind  19926  pf1ind  19936  elply2  20076  plyss  20079  plyeq0lem  20090  taylfval  20236  umgra1  21322  uslgra1  21353  usgra1  21354  usgra1v  21370  cusgra1v  21431  uvtx01vtx  21462  wlkntrl  21523  0pthonv  21542  constr1trl  21549  1pthon  21552  1pthon2v  21554  1conngra  21623  vdgr1d  21635  vdgr1b  21636  vdgr1a  21638  grposn  21764  zrdivrng  21981  0ofval  22249  esumpr  24418  esumfzf  24420  prsiga  24475  cntnevol  24543  subfacp1lem5  24831  erdszelem5  24842  erdszelem8  24845  cvmliftlem4  24936  cvmliftlem5  24937  cvmlift2lem6  24956  cvmlift2lem9  24959  cvmlift2lem12  24962  wfrlem15  25492  fobigcup  25662  elsingles  25679  fnsingle  25680  fvsingle  25681  dfiota3  25684  brapply  25699  brsuccf  25702  funpartlem  25703  altopthsn  25718  altxpsspw  25734  axlowdimlem15  25807  axlowdim  25812  hfsn  26032  onpsstopbas  26092  neibastop2lem  26287  topjoin  26292  fdc  26347  heiborlem3  26420  heiborlem8  26425  ismrer1  26445  ralxpmap  26640  elrfi  26646  mzpincl  26689  mzpcompact2lem  26706  wopprc  26999  dfac11  27036  kelac2  27039  pwssplit3  27066  pwslnmlem1  27070  pwslnm  27072  enfixsn  27133  islindf4  27184  fnchoice  27575  snelpwrVD  28661  bnj918  28853  bnj95  28953  bnj1452  29139  bnj1489  29143  ldualset  29620  lineset  30232  ispointN  30236  dvaset  31499  dvhset  31576  dibval  31637  dibfna  31649
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-v 2926  df-dif 3291  df-un 3293  df-nul 3597  df-sn 3788  df-pr 3789
  Copyright terms: Public domain W3C validator