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

Theorem snex 4154
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4134. (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
StepHypRef Expression
1 dfsn2 3595 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3649 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 629 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2322 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4153 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 2794 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2340 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3636 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 188 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4090 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2344 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 158 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 5    = wceq 1619    e. wcel 1621   _Vcvv 2740   (/)c0 3397   {csn 3581   {cpr 3582
This theorem is referenced by:  prex  4155  elALT  4156  dtruALT2  4157  snelpwi  4158  snelpw  4159  rext  4160  sspwb  4161  intid  4169  moabex  4170  nnullss  4172  exss  4173  opi1  4177  opnz  4179  opeqsn  4199  opeqpr  4200  opthwiener  4205  uniop  4206  frirr  4307  tpex  4456  snnex  4461  op1stb  4506  sucexb  4537  frsn  4713  onnev  4723  xpsspwOLD  4751  relop  4787  soex  5075  elxp4  5112  elxp5  5113  funopg  5190  opabex3  5668  1stval  6023  2ndval  6024  fo1st  6038  fo2nd  6039  mpt2exxg  6094  cnvf1o  6116  fnse  6131  brtpos2  6139  tposexg  6147  tfrlem12  6338  tfrlem16  6342  mapsn  6742  fvdiagfn  6745  mapsnconst  6746  mapsncnv  6747  mapsnf1o2  6748  elixpsn  6788  ixpsnf1o  6789  mapsnf1o  6790  ensn1  6858  en1b  6862  mapsnen  6871  xpsnen  6879  endisj  6882  xpsnen2g  6888  domunsncan  6895  domunsn  6944  fodomr  6945  disjenex  6952  domssex2  6954  domssex  6955  map2xp  6964  phplem2  6974  isinf  7009  pssnn  7014  findcard2  7031  ac6sfi  7034  xpfi  7061  fodomfi  7068  pwfilem  7083  fisn  7113  marypha1lem  7119  brwdom2  7220  unxpwdom2  7235  elirrv  7244  epfrs  7346  tc2  7360  tcsni  7361  ranksuc  7470  fseqenlem1  7584  dfac5lem2  7684  dfac5lem3  7685  dfac5lem4  7686  kmlem2  7710  cdafn  7728  cdaval  7729  cdaassen  7741  mapcdaen  7743  cdadom1  7745  cdainf  7751  ackbij1lem5  7783  cfsuc  7816  isfin1-3  7945  hsmexlem4  7988  axcc2lem  7995  dcomex  8006  axdc3lem4  8012  axdc4lem  8014  ttukeylem3  8071  brdom7disj  8089  brdom6disj  8090  fpwwe2lem13  8197  canthwe  8206  canthp1lem1  8207  uniwun  8295  rankcf  8332  nn0ex  9903  hashxplem  11315  hashmap  11317  hashbclem  11320  hashf1lem1  11323  climconst2  11952  ramub1lem2  13001  setsvalg  13098  setsid  13114  pwsbas  13313  pwsle  13318  pwssca  13322  pwssnf1o  13324  imasplusg  13347  imasmulr  13348  imasvsca  13350  xpsc  13386  acsfn  13488  isfunc  13665  homaf  13789  homaval  13790  gsum2d2  15152  gsumcom2  15153  dprdz  15192  dprdsn  15198  dprd2da  15204  drngnidl  15908  drnglpir  15932  basdif0  16618  ordtbas  16849  leordtval2  16869  dishaus  17037  discmp  17052  concompid  17084  dis2ndc  17113  dislly  17150  dis1stc  17152  1stckgen  17176  ptbasfi  17203  dfac14lem  17238  dfac14  17239  ptrescn  17260  xkoptsub  17275  pt1hmeo  17424  xpstopnlem1  17427  ptcmpfi  17431  isufil2  17530  ufileu  17541  filufint  17542  uffix  17543  uffixsn  17547  flimclslem  17606  ptcmplem1  17673  imasdsf1olem  17864  icccmplem1  18254  icccmplem2  18255  evlssca  19333  mpfind  19355  pf1ind  19365  elply2  19505  plyss  19508  plyeq0lem  19519  taylfval  19665  grposn  20807  zrdivrng  21024  0ofval  21290  subfacp1lem5  23052  erdszelem5  23063  erdszelem8  23066  cvmliftlem4  23156  cvmliftlem5  23157  cvmlift2lem6  23176  cvmlift2lem9  23179  cvmlift2lem12  23182  umgra1  23215  vdgr1d  23231  vdgr1b  23232  vdgr1a  23234  wfrlem15  23604  fobigcup  23781  elsingles  23797  fnsingle  23798  fvsingle  23799  brapply  23817  funpartfv  23823  altopthsn  23835  altxpsspw  23851  axlowdimlem15  23924  axlowdim  23929  hfsn  24149  onpsstopbas  24209  cbicp  24498  basexre  24854  1alg  25054  1ded  25070  1cat  25091  vtare  25217  smbkle  25375  neibastop2lem  25641  topjoin  25646  fdc  25787  heiborlem3  25869  heiborlem8  25874  ismrer1  25894  ralxpmap  26093  elrfi  26101  mzpincl  26144  mzpcompact2lem  26161  wopprc  26455  dfac11  26492  kelac2  26495  pwssplit3  26522  pwslnmlem1  26526  pwslnm  26528  enfixsn  26589  islindf4  26640  fnchoice  27033  snelpwrVD  27619  bnj918  27808  bnj95  27908  bnj153  27924  bnj1452  28094  bnj1489  28098  lsatset  28310  ldualset  28445  lineset  29057  ispointN  29061  dvaset  30324  dvhset  30401  dibval  30462  dibfna  30474
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-v 2742  df-dif 3097  df-un 3099  df-nul 3398  df-sn 3587  df-pr 3588
  Copyright terms: Public domain W3C validator