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

Theorem snex 4407
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4387. (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 3830 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3887 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 628 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2504 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4406 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 3013 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2522 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3873 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 188 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4341 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2526 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 159 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1653    e. wcel 1726   _Vcvv 2958   (/)c0 3630   {csn 3816   {cpr 3817
This theorem is referenced by:  prex  4408  elALT  4409  dtruALT2  4410  snelpwi  4411  snelpw  4412  rext  4414  sspwb  4415  intid  4423  moabex  4424  nnullss  4427  exss  4428  opi1  4432  opnz  4434  opeqsn  4454  opeqpr  4455  opthwiener  4460  uniop  4461  frirr  4561  tpex  4710  snnex  4715  op1stb  4760  sucexb  4791  frsn  4950  onnev  4960  xpsspwOLD  4989  relop  5025  soex  5321  elxp4  5359  elxp5  5360  funopg  5487  opabex3d  5991  opabex3  5992  1stval  6353  2ndval  6354  fo1st  6368  fo2nd  6369  mpt2exxg  6424  cnvf1o  6447  fnse  6465  brtpos2  6487  tfrlem12  6652  tfrlem16  6656  mapsn  7057  fvdiagfn  7060  mapsnconst  7061  mapsncnv  7062  mapsnf1o2  7063  elixpsn  7103  ixpsnf1o  7104  mapsnf1o  7105  ensn1  7173  en1b  7177  mapsnen  7186  xpsnen  7194  endisj  7197  xpsnen2g  7203  domunsncan  7210  domunsn  7259  fodomr  7260  disjenex  7267  domssex2  7269  domssex  7270  map2xp  7279  phplem2  7289  isinf  7324  pssnn  7329  findcard2  7350  ac6sfi  7353  xpfi  7380  fodomfi  7387  pwfilem  7403  fisn  7434  marypha1lem  7440  brwdom2  7543  unxpwdom2  7558  elirrv  7567  epfrs  7669  tc2  7683  tcsni  7684  ranksuc  7793  fseqenlem1  7907  dfac5lem2  8007  dfac5lem3  8008  dfac5lem4  8009  kmlem2  8033  cdafn  8051  cdaval  8052  cdaassen  8064  mapcdaen  8066  cdadom1  8068  cdainf  8074  ackbij1lem5  8106  cfsuc  8139  isfin1-3  8268  hsmexlem4  8311  axcc2lem  8318  dcomex  8329  axdc3lem4  8335  axdc4lem  8337  ttukeylem3  8393  brdom7disj  8411  brdom6disj  8412  fpwwe2lem13  8519  canthwe  8528  canthp1lem1  8529  uniwun  8617  rankcf  8654  nn0ex  10229  hashxplem  11698  hashmap  11700  hashbclem  11703  hashf1lem1  11706  climconst2  12344  incexclem  12618  ramub1lem2  13397  setsvalg  13494  setsid  13510  pwsbas  13711  pwsle  13716  pwssca  13720  pwssnf1o  13722  imasplusg  13745  imasmulr  13746  imasvsca  13748  xpsc  13784  acsfn  13886  isfunc  14063  homaf  14187  homaval  14188  gsum2d2  15550  gsumcom2  15551  dprdz  15590  dprdsn  15596  dprd2da  15602  drngnidl  16302  drnglpir  16326  basdif0  17020  ordtbas  17258  leordtval2  17278  dishaus  17448  discmp  17463  concompid  17496  dis2ndc  17525  dislly  17562  dis1stc  17564  1stckgen  17588  ptbasfi  17615  dfac14lem  17651  dfac14  17652  ptrescn  17673  xkoptsub  17688  pt1hmeo  17840  xpstopnlem1  17843  ptcmpfi  17847  isufil2  17942  ufileu  17953  filufint  17954  uffix  17955  uffixsn  17959  flimclslem  18018  ptcmplem1  18085  cnextfval  18095  imasdsf1olem  18405  icccmplem1  18855  icccmplem2  18856  evlssca  19945  mpfind  19967  pf1ind  19977  elply2  20117  plyss  20120  plyeq0lem  20131  taylfval  20277  umgra1  21363  uslgra1  21394  usgra1  21395  usgra1v  21411  cusgra1v  21472  uvtx01vtx  21503  wlkntrl  21564  0pthonv  21583  constr1trl  21590  1pthon  21593  1pthon2v  21595  1conngra  21664  vdgr1d  21676  vdgr1b  21677  vdgr1a  21679  grposn  21805  zrdivrng  22022  0ofval  22290  esumpr  24459  esumfzf  24461  prsiga  24516  cntnevol  24584  subfacp1lem5  24872  erdszelem5  24883  erdszelem8  24886  cvmliftlem4  24977  cvmliftlem5  24978  cvmlift2lem6  24997  cvmlift2lem9  25000  cvmlift2lem12  25003  wfrlem15  25554  fobigcup  25747  elsingles  25765  fnsingle  25766  fvsingle  25767  dfiota3  25770  brapply  25785  brsuccf  25788  funpartlem  25789  altopthsn  25808  altxpsspw  25824  axlowdimlem15  25897  axlowdim  25902  hfsn  26122  onpsstopbas  26182  neibastop2lem  26391  topjoin  26396  fdc  26451  heiborlem3  26524  heiborlem8  26529  ismrer1  26549  ralxpmap  26744  elrfi  26750  mzpincl  26793  mzpcompact2lem  26810  wopprc  27103  dfac11  27139  kelac2  27142  pwssplit3  27169  pwslnmlem1  27173  pwslnm  27175  enfixsn  27236  islindf4  27287  fnchoice  27678  cshwsex  28309  snelpwrVD  29005  bnj918  29197  bnj95  29297  bnj1452  29483  bnj1489  29487  ldualset  29985  lineset  30597  ispointN  30601  dvaset  31864  dvhset  31941  dibval  32002  dibfna  32014
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2960  df-dif 3325  df-un 3327  df-nul 3631  df-sn 3822  df-pr 3823
  Copyright terms: Public domain W3C validator