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

Theorem snex 4232
Description: A singleton is a set. Theorem 7.13 of [Quine] p. 51, proved using Extensionality, Separation, and Pairing. See also snexALT 4212. (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 3667 . . 3  |-  { A }  =  { A ,  A }
2 preq12 3721 . . . . . 6  |-  ( ( x  =  A  /\  x  =  A )  ->  { x ,  x }  =  { A ,  A } )
32anidms 626 . . . . 5  |-  ( x  =  A  ->  { x ,  x }  =  { A ,  A }
)
43eleq1d 2362 . . . 4  |-  ( x  =  A  ->  ( { x ,  x }  e.  _V  <->  { A ,  A }  e.  _V ) )
5 zfpair2 4231 . . . 4  |-  { x ,  x }  e.  _V
64, 5vtoclg 2856 . . 3  |-  ( A  e.  _V  ->  { A ,  A }  e.  _V )
71, 6syl5eqel 2380 . 2  |-  ( A  e.  _V  ->  { A }  e.  _V )
8 snprc 3708 . . . 4  |-  ( -.  A  e.  _V  <->  { A }  =  (/) )
98biimpi 186 . . 3  |-  ( -.  A  e.  _V  ->  { A }  =  (/) )
10 0ex 4166 . . 3  |-  (/)  e.  _V
119, 10syl6eqel 2384 . 2  |-  ( -.  A  e.  _V  ->  { A }  e.  _V )
127, 11pm2.61i 156 1  |-  { A }  e.  _V
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1632    e. wcel 1696   _Vcvv 2801   (/)c0 3468   {csn 3653   {cpr 3654
This theorem is referenced by:  prex  4233  elALT  4234  dtruALT2  4235  snelpwi  4236  snelpw  4237  rext  4238  sspwb  4239  intid  4247  moabex  4248  nnullss  4251  exss  4252  opi1  4256  opnz  4258  opeqsn  4278  opeqpr  4279  opthwiener  4284  uniop  4285  frirr  4386  tpex  4535  snnex  4540  op1stb  4585  sucexb  4616  frsn  4776  onnev  4786  xpsspwOLD  4814  relop  4850  soex  5138  elxp4  5176  elxp5  5177  funopg  5302  opabex3  5785  1stval  6140  2ndval  6141  fo1st  6155  fo2nd  6156  mpt2exxg  6211  cnvf1o  6233  fnse  6248  brtpos2  6256  tposexg  6264  tfrlem12  6421  tfrlem16  6425  mapsn  6825  fvdiagfn  6828  mapsnconst  6829  mapsncnv  6830  mapsnf1o2  6831  elixpsn  6871  ixpsnf1o  6872  mapsnf1o  6873  ensn1  6941  en1b  6945  mapsnen  6954  xpsnen  6962  endisj  6965  xpsnen2g  6971  domunsncan  6978  domunsn  7027  fodomr  7028  disjenex  7035  domssex2  7037  domssex  7038  map2xp  7047  phplem2  7057  isinf  7092  pssnn  7097  findcard2  7114  ac6sfi  7117  xpfi  7144  fodomfi  7151  pwfilem  7166  fisn  7196  marypha1lem  7202  brwdom2  7303  unxpwdom2  7318  elirrv  7327  epfrs  7429  tc2  7443  tcsni  7444  ranksuc  7553  fseqenlem1  7667  dfac5lem2  7767  dfac5lem3  7768  dfac5lem4  7769  kmlem2  7793  cdafn  7811  cdaval  7812  cdaassen  7824  mapcdaen  7826  cdadom1  7828  cdainf  7834  ackbij1lem5  7866  cfsuc  7899  isfin1-3  8028  hsmexlem4  8071  axcc2lem  8078  dcomex  8089  axdc3lem4  8095  axdc4lem  8097  ttukeylem3  8154  brdom7disj  8172  brdom6disj  8173  fpwwe2lem13  8280  canthwe  8289  canthp1lem1  8290  uniwun  8378  rankcf  8415  nn0ex  9987  hashxplem  11401  hashmap  11403  hashbclem  11406  hashf1lem1  11409  climconst2  12038  incexclem  12311  ramub1lem2  13090  setsvalg  13187  setsid  13203  pwsbas  13402  pwsle  13407  pwssca  13411  pwssnf1o  13413  imasplusg  13436  imasmulr  13437  imasvsca  13439  xpsc  13475  acsfn  13577  isfunc  13754  homaf  13878  homaval  13879  gsum2d2  15241  gsumcom2  15242  dprdz  15281  dprdsn  15287  dprd2da  15293  drngnidl  15997  drnglpir  16021  basdif0  16707  ordtbas  16938  leordtval2  16958  dishaus  17126  discmp  17141  concompid  17173  dis2ndc  17202  dislly  17239  dis1stc  17241  1stckgen  17265  ptbasfi  17292  dfac14lem  17327  dfac14  17328  ptrescn  17349  xkoptsub  17364  pt1hmeo  17513  xpstopnlem1  17516  ptcmpfi  17520  isufil2  17619  ufileu  17630  filufint  17631  uffix  17632  uffixsn  17636  flimclslem  17695  ptcmplem1  17762  imasdsf1olem  17953  icccmplem1  18343  icccmplem2  18344  evlssca  19422  mpfind  19444  pf1ind  19454  elply2  19594  plyss  19597  plyeq0lem  19608  taylfval  19754  grposn  20898  zrdivrng  21115  0ofval  21381  cntnevol  23191  esumpr  23453  prsiga  23507  subfacp1lem5  23730  erdszelem5  23741  erdszelem8  23744  cvmliftlem4  23834  cvmliftlem5  23835  cvmlift2lem6  23854  cvmlift2lem9  23857  cvmlift2lem12  23860  umgra1  23893  vdgr1d  23909  vdgr1b  23910  vdgr1a  23912  wfrlem15  24341  fobigcup  24511  elsingles  24528  fnsingle  24529  fvsingle  24530  dfiota3  24533  brapply  24548  brsuccf  24551  funpartlem  24552  altopthsn  24567  altxpsspw  24583  axlowdimlem15  24656  axlowdim  24661  hfsn  24881  onpsstopbas  24941  cbicp  25269  basexre  25625  1alg  25825  1ded  25841  1cat  25862  vtare  25988  smbkle  26146  cndpv  26152  pgapspf  26155  lineval222  26182  lineval3a  26186  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  neibastop2lem  26412  topjoin  26417  fdc  26558  heiborlem3  26640  heiborlem8  26645  ismrer1  26665  ralxpmap  26864  elrfi  26872  mzpincl  26915  mzpcompact2lem  26932  wopprc  27226  dfac11  27263  kelac2  27266  pwssplit3  27293  pwslnmlem1  27297  pwslnm  27299  enfixsn  27360  islindf4  27411  fnchoice  27803  opabex3d  28190  uslgra1  28252  usgra1  28253  usgra1v  28260  cusgra1v  28296  uvtx01vtx  28305  wlkntrl  28350  snelpwrVD  28922  bnj918  29112  bnj95  29212  bnj153  29228  bnj1452  29398  bnj1489  29402  lsatset  29802  ldualset  29937  lineset  30549  ispointN  30553  dvaset  31816  dvhset  31893  dibval  31954  dibfna  31966
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-un 3170  df-nul 3469  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator